| author | wenzelm |
| Tue, 29 May 2012 16:39:42 +0200 | |
| changeset 48014 | 63021e59cbf0 |
| child 48550 | 97592027a2a8 |
| permissions | -rw-r--r-- |
|
48014
63021e59cbf0
separate README dockable, which allows to make it more prominent first and remove it later;
wenzelm
parents:
diff
changeset
|
1 |
/* Title: Tools/jEdit/src/readme_dockable.scala |
|
63021e59cbf0
separate README dockable, which allows to make it more prominent first and remove it later;
wenzelm
parents:
diff
changeset
|
2 |
Author: Makarius |
|
63021e59cbf0
separate README dockable, which allows to make it more prominent first and remove it later;
wenzelm
parents:
diff
changeset
|
3 |
|
|
63021e59cbf0
separate README dockable, which allows to make it more prominent first and remove it later;
wenzelm
parents:
diff
changeset
|
4 |
Dockable window for README. |
|
63021e59cbf0
separate README dockable, which allows to make it more prominent first and remove it later;
wenzelm
parents:
diff
changeset
|
5 |
*/ |
|
63021e59cbf0
separate README dockable, which allows to make it more prominent first and remove it later;
wenzelm
parents:
diff
changeset
|
6 |
|
|
63021e59cbf0
separate README dockable, which allows to make it more prominent first and remove it later;
wenzelm
parents:
diff
changeset
|
7 |
package isabelle.jedit |
|
63021e59cbf0
separate README dockable, which allows to make it more prominent first and remove it later;
wenzelm
parents:
diff
changeset
|
8 |
|
|
63021e59cbf0
separate README dockable, which allows to make it more prominent first and remove it later;
wenzelm
parents:
diff
changeset
|
9 |
|
|
63021e59cbf0
separate README dockable, which allows to make it more prominent first and remove it later;
wenzelm
parents:
diff
changeset
|
10 |
import isabelle._ |
|
63021e59cbf0
separate README dockable, which allows to make it more prominent first and remove it later;
wenzelm
parents:
diff
changeset
|
11 |
|
|
63021e59cbf0
separate README dockable, which allows to make it more prominent first and remove it later;
wenzelm
parents:
diff
changeset
|
12 |
import org.gjt.sp.jedit.View |
|
63021e59cbf0
separate README dockable, which allows to make it more prominent first and remove it later;
wenzelm
parents:
diff
changeset
|
13 |
|
|
63021e59cbf0
separate README dockable, which allows to make it more prominent first and remove it later;
wenzelm
parents:
diff
changeset
|
14 |
|
|
63021e59cbf0
separate README dockable, which allows to make it more prominent first and remove it later;
wenzelm
parents:
diff
changeset
|
15 |
class README_Dockable(view: View, position: String) extends Dockable(view: View, position: String) |
|
63021e59cbf0
separate README dockable, which allows to make it more prominent first and remove it later;
wenzelm
parents:
diff
changeset
|
16 |
{
|
|
63021e59cbf0
separate README dockable, which allows to make it more prominent first and remove it later;
wenzelm
parents:
diff
changeset
|
17 |
private val readme = new HTML_Panel("SansSerif", 14)
|
|
63021e59cbf0
separate README dockable, which allows to make it more prominent first and remove it later;
wenzelm
parents:
diff
changeset
|
18 |
private val readme_path = Path.explode("$JEDIT_HOME/README.html")
|
|
63021e59cbf0
separate README dockable, which allows to make it more prominent first and remove it later;
wenzelm
parents:
diff
changeset
|
19 |
readme.render_document( |
|
63021e59cbf0
separate README dockable, which allows to make it more prominent first and remove it later;
wenzelm
parents:
diff
changeset
|
20 |
Isabelle_System.platform_file_url(readme_path), |
|
63021e59cbf0
separate README dockable, which allows to make it more prominent first and remove it later;
wenzelm
parents:
diff
changeset
|
21 |
Isabelle_System.try_read(List(readme_path))) |
|
63021e59cbf0
separate README dockable, which allows to make it more prominent first and remove it later;
wenzelm
parents:
diff
changeset
|
22 |
|
|
63021e59cbf0
separate README dockable, which allows to make it more prominent first and remove it later;
wenzelm
parents:
diff
changeset
|
23 |
set_content(readme) |
|
63021e59cbf0
separate README dockable, which allows to make it more prominent first and remove it later;
wenzelm
parents:
diff
changeset
|
24 |
} |