equal
deleted
inserted
replaced
2467 "Modified: / 16-08-2017 / 13:57:36 / cg" |
2467 "Modified: / 16-08-2017 / 13:57:36 / cg" |
2468 "Modified: / 30-10-2018 / 16:22:13 / Claus Gittinger" |
2468 "Modified: / 30-10-2018 / 16:22:13 / Claus Gittinger" |
2469 ! |
2469 ! |
2470 |
2470 |
2471 openDocumentation |
2471 openDocumentation |
|
2472 "Called when <F1> is pressed" |
|
2473 |
2472 HTMLDocumentView openFullOnDocumentationFile:'tools/misc/TOP.html#VIEWTREEINSPECTOR' |
2474 HTMLDocumentView openFullOnDocumentationFile:'tools/misc/TOP.html#VIEWTREEINSPECTOR' |
2473 ! |
2475 ! |
2474 |
2476 |
2475 showWindow:aView |
2477 showWindow:aView |
2476 "show a particular window's topView hierarchy, |
2478 "show a particular window's topView hierarchy, |