isabelle: src/Tools/jEdit/src/readme_dockable.scala@ec6011bf2362 (annotated)

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
49559 c3a6e110679b tuned; wenzelm parents: 48550 diff changeset	15	class README_Dockable(view: View, position: String) extends Dockable(view, position)
48014 63021e59cbf0 separate README dockable, which allows to make it more prominent first and remove it later; wenzelm parents: diff changeset	16	{
49612 e6a53d203362 eliminated obsolete HTML/CSS functionality; wenzelm parents: 49559 diff changeset	17	private val readme = new HTML_Panel
48014 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")
49612 e6a53d203362 eliminated obsolete HTML/CSS functionality; wenzelm parents: 49559 diff changeset	19	readme.render_document(Isabelle_System.platform_file_url(readme_path), File.read(readme_path))
48014 63021e59cbf0 separate README dockable, which allows to make it more prominent first and remove it later; wenzelm parents: diff changeset	20
63021e59cbf0 separate README dockable, which allows to make it more prominent first and remove it later; wenzelm parents: diff changeset	21	set_content(readme)
63021e59cbf0 separate README dockable, which allows to make it more prominent first and remove it later; wenzelm parents: diff changeset	22	}

author	wenzelm
	Wed, 28 Aug 2013 09:36:05 +0200
changeset 53244	ec6011bf2362
parent 53177	dcac8d837b9c
permissions	-rw-r--r--