isabelle: src/Tools/jEdit/src/plugin.scala@24444588fddd (annotated)

43282 5d294220ca43 moved sources -- eliminated Netbeans artifact of jedit package directory; wenzelm parents: 41537 diff changeset	1	/* Title: Tools/jEdit/src/plugin.scala
36760 b82a698ef6c9 tuned headers; wenzelm parents: 36015 diff changeset	2	Author: Makarius
b82a698ef6c9 tuned headers; wenzelm parents: 36015 diff changeset	3
b82a698ef6c9 tuned headers; wenzelm parents: 36015 diff changeset	4	Main Isabelle/jEdit plugin setup.
b82a698ef6c9 tuned headers; wenzelm parents: 36015 diff changeset	5	*/
34407 aad6834ba380 added some headers and comments; wenzelm parents: 34406 diff changeset	6
34318 c13e168a8ae6 original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout; wenzelm parents: diff changeset	7	package isabelle.jedit
c13e168a8ae6 original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout; wenzelm parents: diff changeset	8
34429 03afc73e185f tuned; wenzelm parents: 34422 diff changeset	9
36015 6111de7c916a adapted to Scala 2.8.0 Beta 1; wenzelm parents: 34871 diff changeset	10	import isabelle._
6111de7c916a adapted to Scala 2.8.0 Beta 1; wenzelm parents: 34871 diff changeset	11
43520 cec9b95fa35d explicit import java.lang.System to prevent odd scope problems; wenzelm parents: 43513 diff changeset	12	import java.lang.System
43645 ac886d096c11 some support for Session.File_Store; wenzelm parents: 43643 diff changeset	13	import java.io.{File, FileInputStream, IOException}
34318 c13e168a8ae6 original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout; wenzelm parents: diff changeset	14	import java.awt.Font
44573 51f8895b9ad9 some dialog for auto loading of required files (still inactive); wenzelm parents: 44434 diff changeset	15	import javax.swing.JOptionPane
44574 24444588fddd actual auto loading of required files; wenzelm parents: 44573 diff changeset	16	import javax.swing.text.Segment
34318 c13e168a8ae6 original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout; wenzelm parents: diff changeset	17
34497 184fda8cce04 more explicit indication of mutable collections; wenzelm parents: 34487 diff changeset	18	import scala.collection.mutable
39517 e036c67448e6 separate Isabelle.logic_selector; wenzelm parents: 39515 diff changeset	19	import scala.swing.ComboBox
44574 24444588fddd actual auto loading of required files; wenzelm parents: 44573 diff changeset	20	import scala.util.Sorting
34406 f81cd75ae331 restructured: independent provers in different buffers immler@in.tum.de parents: 34337 diff changeset	21
39241 e9a442606db3 Isabelle.load_icon with some sanity checks; wenzelm parents: 39167 diff changeset	22	import org.gjt.sp.jedit.{jEdit, GUIUtilities, EBMessage, EBPlugin,
43645 ac886d096c11 some support for Session.File_Store; wenzelm parents: 43643 diff changeset	23	Buffer, EditPane, MiscUtilities, ServiceManager, View}
34406 f81cd75ae331 restructured: independent provers in different buffers immler@in.tum.de parents: 34337 diff changeset	24	import org.gjt.sp.jedit.buffer.JEditBuffer
39043 a0d7e9b580ec added gfx_range convenience; wenzelm parents: 38854 diff changeset	25	import org.gjt.sp.jedit.textarea.{JEditTextArea, TextArea}
43452 5cf548485529 avoid setTokenMarker fluctuation on buffer reload etc. via static isabelle_token_marker, which is installed by hijacking the jEdit ModeProvider; wenzelm parents: 43449 diff changeset	26	import org.gjt.sp.jedit.syntax.{Token => JEditToken, ModeProvider}
39633 26a28110ece5 simplified Session.Phase; wenzelm parents: 39631 diff changeset	27	import org.gjt.sp.jedit.msg.{EditorStarted, BufferUpdate, EditPaneUpdate, PropertiesChanged}
37068 07936a4efe93 access statically typed dockable windows; wenzelm parents: 37019 diff changeset	28	import org.gjt.sp.jedit.gui.DockableWindowManager
44160 8848867501fb clarified document model header: master_dir (native wrt. editor, potentially URL) and node_name (full canonical path); wenzelm parents: 43714 diff changeset	29	import org.gjt.sp.jedit.io.{VFS, FileVFS, VFSManager}
34429 03afc73e185f tuned; wenzelm parents: 34422 diff changeset	30
43443 5d9693c2337e basic support for extended syntax styles: sub/superscript; wenzelm parents: 43390 diff changeset	31	import org.gjt.sp.util.SyntaxUtilities
39241 e9a442606db3 Isabelle.load_icon with some sanity checks; wenzelm parents: 39167 diff changeset	32	import org.gjt.sp.util.Log
e9a442606db3 Isabelle.load_icon with some sanity checks; wenzelm parents: 39167 diff changeset	33
39630 44181423183a explicit Session.Phase indication with associated event bus; wenzelm parents: 39628 diff changeset	34	import scala.actors.Actor
44181423183a explicit Session.Phase indication with associated event bus; wenzelm parents: 39628 diff changeset	35	import Actor._
44181423183a explicit Session.Phase indication with associated event bus; wenzelm parents: 39628 diff changeset	36
34318 c13e168a8ae6 original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout; wenzelm parents: diff changeset	37
34618 e45052ff7233 added Boolean_Property, Int_Property; wenzelm parents: 34615 diff changeset	38	object Isabelle
e45052ff7233 added Boolean_Property, Int_Property; wenzelm parents: 34615 diff changeset	39	{
34784 02959dcea756 split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea); wenzelm parents: 34782 diff changeset	40	/* plugin instance */
02959dcea756 split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea); wenzelm parents: 34782 diff changeset	41
43443 5d9693c2337e basic support for extended syntax styles: sub/superscript; wenzelm parents: 43390 diff changeset	42	var plugin: Plugin = null
34784 02959dcea756 split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea); wenzelm parents: 34782 diff changeset	43	var session: Session = null
02959dcea756 split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea); wenzelm parents: 34782 diff changeset	44
02959dcea756 split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea); wenzelm parents: 34782 diff changeset	45
34618 e45052ff7233 added Boolean_Property, Int_Property; wenzelm parents: 34615 diff changeset	46	/* properties */
e45052ff7233 added Boolean_Property, Int_Property; wenzelm parents: 34615 diff changeset	47
e45052ff7233 added Boolean_Property, Int_Property; wenzelm parents: 34615 diff changeset	48	val OPTION_PREFIX = "options.isabelle."
e45052ff7233 added Boolean_Property, Int_Property; wenzelm parents: 34615 diff changeset	49
e45052ff7233 added Boolean_Property, Int_Property; wenzelm parents: 34615 diff changeset	50	object Property
e45052ff7233 added Boolean_Property, Int_Property; wenzelm parents: 34615 diff changeset	51	{
36814 dc85664dbf6d support Isabelle plugin properties with defaults; wenzelm parents: 36760 diff changeset	52	def apply(name: String): String =
dc85664dbf6d support Isabelle plugin properties with defaults; wenzelm parents: 36760 diff changeset	53	jEdit.getProperty(OPTION_PREFIX + name)
dc85664dbf6d support Isabelle plugin properties with defaults; wenzelm parents: 36760 diff changeset	54	def apply(name: String, default: String): String =
dc85664dbf6d support Isabelle plugin properties with defaults; wenzelm parents: 36760 diff changeset	55	jEdit.getProperty(OPTION_PREFIX + name, default)
dc85664dbf6d support Isabelle plugin properties with defaults; wenzelm parents: 36760 diff changeset	56	def update(name: String, value: String) =
dc85664dbf6d support Isabelle plugin properties with defaults; wenzelm parents: 36760 diff changeset	57	jEdit.setProperty(OPTION_PREFIX + name, value)
34468 9d4b4f290676 maintain Isabelle properties via object Isabelle.Property with apply/update methods; wenzelm parents: 34463 diff changeset	58	}
34433 3da749b53842 renamed Plugin.plugin to Plugin.self; wenzelm parents: 34429 diff changeset	59
34618 e45052ff7233 added Boolean_Property, Int_Property; wenzelm parents: 34615 diff changeset	60	object Boolean_Property
e45052ff7233 added Boolean_Property, Int_Property; wenzelm parents: 34615 diff changeset	61	{
36814 dc85664dbf6d support Isabelle plugin properties with defaults; wenzelm parents: 36760 diff changeset	62	def apply(name: String): Boolean =
dc85664dbf6d support Isabelle plugin properties with defaults; wenzelm parents: 36760 diff changeset	63	jEdit.getBooleanProperty(OPTION_PREFIX + name)
dc85664dbf6d support Isabelle plugin properties with defaults; wenzelm parents: 36760 diff changeset	64	def apply(name: String, default: Boolean): Boolean =
dc85664dbf6d support Isabelle plugin properties with defaults; wenzelm parents: 36760 diff changeset	65	jEdit.getBooleanProperty(OPTION_PREFIX + name, default)
dc85664dbf6d support Isabelle plugin properties with defaults; wenzelm parents: 36760 diff changeset	66	def update(name: String, value: Boolean) =
dc85664dbf6d support Isabelle plugin properties with defaults; wenzelm parents: 36760 diff changeset	67	jEdit.setBooleanProperty(OPTION_PREFIX + name, value)
34618 e45052ff7233 added Boolean_Property, Int_Property; wenzelm parents: 34615 diff changeset	68	}
e45052ff7233 added Boolean_Property, Int_Property; wenzelm parents: 34615 diff changeset	69
e45052ff7233 added Boolean_Property, Int_Property; wenzelm parents: 34615 diff changeset	70	object Int_Property
e45052ff7233 added Boolean_Property, Int_Property; wenzelm parents: 34615 diff changeset	71	{
36814 dc85664dbf6d support Isabelle plugin properties with defaults; wenzelm parents: 36760 diff changeset	72	def apply(name: String): Int =
dc85664dbf6d support Isabelle plugin properties with defaults; wenzelm parents: 36760 diff changeset	73	jEdit.getIntegerProperty(OPTION_PREFIX + name)
dc85664dbf6d support Isabelle plugin properties with defaults; wenzelm parents: 36760 diff changeset	74	def apply(name: String, default: Int): Int =
dc85664dbf6d support Isabelle plugin properties with defaults; wenzelm parents: 36760 diff changeset	75	jEdit.getIntegerProperty(OPTION_PREFIX + name, default)
dc85664dbf6d support Isabelle plugin properties with defaults; wenzelm parents: 36760 diff changeset	76	def update(name: String, value: Int) =
dc85664dbf6d support Isabelle plugin properties with defaults; wenzelm parents: 36760 diff changeset	77	jEdit.setIntegerProperty(OPTION_PREFIX + name, value)
34618 e45052ff7233 added Boolean_Property, Int_Property; wenzelm parents: 34615 diff changeset	78	}
e45052ff7233 added Boolean_Property, Int_Property; wenzelm parents: 34615 diff changeset	79
40848 8662b9b1f123 more abstract/uniform handling of time, preferring seconds as Double; wenzelm parents: 40474 diff changeset	80	object Double_Property
8662b9b1f123 more abstract/uniform handling of time, preferring seconds as Double; wenzelm parents: 40474 diff changeset	81	{
8662b9b1f123 more abstract/uniform handling of time, preferring seconds as Double; wenzelm parents: 40474 diff changeset	82	def apply(name: String): Double =
8662b9b1f123 more abstract/uniform handling of time, preferring seconds as Double; wenzelm parents: 40474 diff changeset	83	jEdit.getDoubleProperty(OPTION_PREFIX + name, 0.0)
8662b9b1f123 more abstract/uniform handling of time, preferring seconds as Double; wenzelm parents: 40474 diff changeset	84	def apply(name: String, default: Double): Double =
8662b9b1f123 more abstract/uniform handling of time, preferring seconds as Double; wenzelm parents: 40474 diff changeset	85	jEdit.getDoubleProperty(OPTION_PREFIX + name, default)
8662b9b1f123 more abstract/uniform handling of time, preferring seconds as Double; wenzelm parents: 40474 diff changeset	86	def update(name: String, value: Double) =
8662b9b1f123 more abstract/uniform handling of time, preferring seconds as Double; wenzelm parents: 40474 diff changeset	87	jEdit.setDoubleProperty(OPTION_PREFIX + name, value)
8662b9b1f123 more abstract/uniform handling of time, preferring seconds as Double; wenzelm parents: 40474 diff changeset	88	}
8662b9b1f123 more abstract/uniform handling of time, preferring seconds as Double; wenzelm parents: 40474 diff changeset	89
40850 d804de9ac970 more abstract handling of Time properties; wenzelm parents: 40849 diff changeset	90	object Time_Property
d804de9ac970 more abstract handling of Time properties; wenzelm parents: 40849 diff changeset	91	{
d804de9ac970 more abstract handling of Time properties; wenzelm parents: 40849 diff changeset	92	def apply(name: String): Time =
d804de9ac970 more abstract handling of Time properties; wenzelm parents: 40849 diff changeset	93	Time.seconds(Double_Property(name))
d804de9ac970 more abstract handling of Time properties; wenzelm parents: 40849 diff changeset	94	def apply(name: String, default: Time): Time =
d804de9ac970 more abstract handling of Time properties; wenzelm parents: 40849 diff changeset	95	Time.seconds(Double_Property(name, default.seconds))
d804de9ac970 more abstract handling of Time properties; wenzelm parents: 40849 diff changeset	96	def update(name: String, value: Time) =
d804de9ac970 more abstract handling of Time properties; wenzelm parents: 40849 diff changeset	97	Double_Property.update(name, value.seconds)
d804de9ac970 more abstract handling of Time properties; wenzelm parents: 40849 diff changeset	98	}
d804de9ac970 more abstract handling of Time properties; wenzelm parents: 40849 diff changeset	99
40848 8662b9b1f123 more abstract/uniform handling of time, preferring seconds as Double; wenzelm parents: 40474 diff changeset	100
37164 8b4617ad1593 reuse main view.font from jEdit; wenzelm parents: 37068 diff changeset	101	/* font */
8b4617ad1593 reuse main view.font from jEdit; wenzelm parents: 37068 diff changeset	102
8b4617ad1593 reuse main view.font from jEdit; wenzelm parents: 37068 diff changeset	103	def font_family(): String = jEdit.getProperty("view.font")
8b4617ad1593 reuse main view.font from jEdit; wenzelm parents: 37068 diff changeset	104
37019 8f747cee4e27 zoom font size; wenzelm parents: 36814 diff changeset	105	def font_size(): Float =
8f747cee4e27 zoom font size; wenzelm parents: 36814 diff changeset	106	(jEdit.getIntegerProperty("view.fontsize", 16) *
8f747cee4e27 zoom font size; wenzelm parents: 36814 diff changeset	107	Int_Property("relative-font-size", 100)).toFloat / 100
36814 dc85664dbf6d support Isabelle plugin properties with defaults; wenzelm parents: 36760 diff changeset	108
34618 e45052ff7233 added Boolean_Property, Int_Property; wenzelm parents: 34615 diff changeset	109
39043 a0d7e9b580ec added gfx_range convenience; wenzelm parents: 38854 diff changeset	110	/* text area ranges */
a0d7e9b580ec added gfx_range convenience; wenzelm parents: 38854 diff changeset	111
43714 3749d1e6dde9 tuned signature; wenzelm parents: 43697 diff changeset	112	sealed case class Gfx_Range(val x: Int, val y: Int, val length: Int)
39043 a0d7e9b580ec added gfx_range convenience; wenzelm parents: 38854 diff changeset	113
a0d7e9b580ec added gfx_range convenience; wenzelm parents: 38854 diff changeset	114	def gfx_range(text_area: TextArea, range: Text.Range): Option[Gfx_Range] =
a0d7e9b580ec added gfx_range convenience; wenzelm parents: 38854 diff changeset	115	{
a0d7e9b580ec added gfx_range convenience; wenzelm parents: 38854 diff changeset	116	val p = text_area.offsetToXY(range.start)
a0d7e9b580ec added gfx_range convenience; wenzelm parents: 38854 diff changeset	117	val q = text_area.offsetToXY(range.stop)
a0d7e9b580ec added gfx_range convenience; wenzelm parents: 38854 diff changeset	118	if (p != null && q != null && p.y == q.y) Some(new Gfx_Range(p.x, p.y, q.x - p.x))
a0d7e9b580ec added gfx_range convenience; wenzelm parents: 38854 diff changeset	119	else None
a0d7e9b580ec added gfx_range convenience; wenzelm parents: 38854 diff changeset	120	}
a0d7e9b580ec added gfx_range convenience; wenzelm parents: 38854 diff changeset	121
a0d7e9b580ec added gfx_range convenience; wenzelm parents: 38854 diff changeset	122
37201 8517a650cfdc control tooltip font via Swing HTML, with tooltip-font-size property; wenzelm parents: 37177 diff changeset	123	/* tooltip markup */
8517a650cfdc control tooltip font via Swing HTML, with tooltip-font-size property; wenzelm parents: 37177 diff changeset	124
8517a650cfdc control tooltip font via Swing HTML, with tooltip-font-size property; wenzelm parents: 37177 diff changeset	125	def tooltip(text: String): String =
37203 c4261f3bbdd7 more flexibile font size via CSS <style> instead of old <font> element; wenzelm parents: 37201 diff changeset	126	"<html><pre style=\"font-family: " + font_family() + "; font-size: " +
c4261f3bbdd7 more flexibile font size via CSS <style> instead of old <font> element; wenzelm parents: 37201 diff changeset	127	Int_Property("tooltip-font-size", 10).toString + "px; \">" + // FIXME proper scaling (!?)
c4261f3bbdd7 more flexibile font size via CSS <style> instead of old <font> element; wenzelm parents: 37201 diff changeset	128	HTML.encode(text) + "</pre></html>"
37201 8517a650cfdc control tooltip font via Swing HTML, with tooltip-font-size property; wenzelm parents: 37177 diff changeset	129
40849 09270033330e store tooltip-dismiss-delay as Double(seconds); wenzelm parents: 40848 diff changeset	130	def tooltip_dismiss_delay(): Time =
40852 aee98c88c587 builtin time bounds (again); wenzelm parents: 40850 diff changeset	131	Time_Property("tooltip-dismiss-delay", Time.seconds(8.0)) max Time.seconds(0.5)
38854 eb6a35be18ca Isabelle/jEdit property for global tooltip dismiss delay; wenzelm parents: 38843 diff changeset	132
eb6a35be18ca Isabelle/jEdit property for global tooltip dismiss delay; wenzelm parents: 38843 diff changeset	133	def setup_tooltips()
eb6a35be18ca Isabelle/jEdit property for global tooltip dismiss delay; wenzelm parents: 38843 diff changeset	134	{
eb6a35be18ca Isabelle/jEdit property for global tooltip dismiss delay; wenzelm parents: 38843 diff changeset	135	Swing_Thread.now {
eb6a35be18ca Isabelle/jEdit property for global tooltip dismiss delay; wenzelm parents: 38843 diff changeset	136	val manager = javax.swing.ToolTipManager.sharedInstance
40849 09270033330e store tooltip-dismiss-delay as Double(seconds); wenzelm parents: 40848 diff changeset	137	manager.setDismissDelay(tooltip_dismiss_delay().ms.toInt)
38854 eb6a35be18ca Isabelle/jEdit property for global tooltip dismiss delay; wenzelm parents: 38843 diff changeset	138	}
eb6a35be18ca Isabelle/jEdit property for global tooltip dismiss delay; wenzelm parents: 38843 diff changeset	139	}
eb6a35be18ca Isabelle/jEdit property for global tooltip dismiss delay; wenzelm parents: 38843 diff changeset	140
37201 8517a650cfdc control tooltip font via Swing HTML, with tooltip-font-size property; wenzelm parents: 37177 diff changeset	141
39241 e9a442606db3 Isabelle.load_icon with some sanity checks; wenzelm parents: 39167 diff changeset	142	/* icons */
e9a442606db3 Isabelle.load_icon with some sanity checks; wenzelm parents: 39167 diff changeset	143
e9a442606db3 Isabelle.load_icon with some sanity checks; wenzelm parents: 39167 diff changeset	144	def load_icon(name: String): javax.swing.Icon =
e9a442606db3 Isabelle.load_icon with some sanity checks; wenzelm parents: 39167 diff changeset	145	{
e9a442606db3 Isabelle.load_icon with some sanity checks; wenzelm parents: 39167 diff changeset	146	val icon = GUIUtilities.loadIcon(name)
e9a442606db3 Isabelle.load_icon with some sanity checks; wenzelm parents: 39167 diff changeset	147	if (icon.getIconWidth < 0 \|\| icon.getIconHeight < 0)
39630 44181423183a explicit Session.Phase indication with associated event bus; wenzelm parents: 39628 diff changeset	148	Log.log(Log.ERROR, icon, "Bad icon: " + name)
39241 e9a442606db3 Isabelle.load_icon with some sanity checks; wenzelm parents: 39167 diff changeset	149	icon
e9a442606db3 Isabelle.load_icon with some sanity checks; wenzelm parents: 39167 diff changeset	150	}
e9a442606db3 Isabelle.load_icon with some sanity checks; wenzelm parents: 39167 diff changeset	151
e9a442606db3 Isabelle.load_icon with some sanity checks; wenzelm parents: 39167 diff changeset	152
41382 d19b8388d4b1 explicit JVM check on startup; wenzelm parents: 40852 diff changeset	153	/* check JVM */
d19b8388d4b1 explicit JVM check on startup; wenzelm parents: 40852 diff changeset	154
d19b8388d4b1 explicit JVM check on startup; wenzelm parents: 40852 diff changeset	155	def check_jvm()
d19b8388d4b1 explicit JVM check on startup; wenzelm parents: 40852 diff changeset	156	{
d19b8388d4b1 explicit JVM check on startup; wenzelm parents: 40852 diff changeset	157	if (!Platform.is_hotspot) {
d19b8388d4b1 explicit JVM check on startup; wenzelm parents: 40852 diff changeset	158	Library.warning_dialog(jEdit.getActiveView, "Bad Java Virtual Machine",
d19b8388d4b1 explicit JVM check on startup; wenzelm parents: 40852 diff changeset	159	"This is " + Platform.jvm_name,
d19b8388d4b1 explicit JVM check on startup; wenzelm parents: 40852 diff changeset	160	"Isabelle/jEdit requires Java Hotspot from Sun/Oracle/Apple!")
d19b8388d4b1 explicit JVM check on startup; wenzelm parents: 40852 diff changeset	161	}
d19b8388d4b1 explicit JVM check on startup; wenzelm parents: 40852 diff changeset	162	}
d19b8388d4b1 explicit JVM check on startup; wenzelm parents: 40852 diff changeset	163
d19b8388d4b1 explicit JVM check on startup; wenzelm parents: 40852 diff changeset	164
38221 e0f00f0945b4 misc tuning and clarification; wenzelm parents: 37557 diff changeset	165	/* main jEdit components */
34784 02959dcea756 split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea); wenzelm parents: 34782 diff changeset	166
37177 17331ca75044 avoid deprecated Iterator.fromArray; wenzelm parents: 37164 diff changeset	167	def jedit_buffers(): Iterator[Buffer] = jEdit.getBuffers().iterator
34784 02959dcea756 split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea); wenzelm parents: 34782 diff changeset	168
37177 17331ca75044 avoid deprecated Iterator.fromArray; wenzelm parents: 37164 diff changeset	169	def jedit_views(): Iterator[View] = jEdit.getViews().iterator
34784 02959dcea756 split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea); wenzelm parents: 34782 diff changeset	170
02959dcea756 split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea); wenzelm parents: 34782 diff changeset	171	def jedit_text_areas(view: View): Iterator[JEditTextArea] =
37177 17331ca75044 avoid deprecated Iterator.fromArray; wenzelm parents: 37164 diff changeset	172	view.getEditPanes().iterator.map(_.getTextArea)
34784 02959dcea756 split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea); wenzelm parents: 34782 diff changeset	173
02959dcea756 split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea); wenzelm parents: 34782 diff changeset	174	def jedit_text_areas(): Iterator[JEditTextArea] =
02959dcea756 split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea); wenzelm parents: 34782 diff changeset	175	jedit_views().flatMap(jedit_text_areas(_))
02959dcea756 split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea); wenzelm parents: 34782 diff changeset	176
02959dcea756 split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea); wenzelm parents: 34782 diff changeset	177	def jedit_text_areas(buffer: JEditBuffer): Iterator[JEditTextArea] =
02959dcea756 split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea); wenzelm parents: 34782 diff changeset	178	jedit_text_areas().filter(_.getBuffer == buffer)
02959dcea756 split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea); wenzelm parents: 34782 diff changeset	179
38843 d95522496593 more careful locking of jEdit buffer; wenzelm parents: 38640 diff changeset	180	def buffer_lock[A](buffer: JEditBuffer)(body: => A): A =
38640 105d1f112da5 sporadic locking of jEdit buffer; wenzelm parents: 38222 diff changeset	181	{
105d1f112da5 sporadic locking of jEdit buffer; wenzelm parents: 38222 diff changeset	182	try { buffer.readLock(); body }
105d1f112da5 sporadic locking of jEdit buffer; wenzelm parents: 38222 diff changeset	183	finally { buffer.readUnlock() }
105d1f112da5 sporadic locking of jEdit buffer; wenzelm parents: 38222 diff changeset	184	}
105d1f112da5 sporadic locking of jEdit buffer; wenzelm parents: 38222 diff changeset	185
38843 d95522496593 more careful locking of jEdit buffer; wenzelm parents: 38640 diff changeset	186	def swing_buffer_lock[A](buffer: JEditBuffer)(body: => A): A =
d95522496593 more careful locking of jEdit buffer; wenzelm parents: 38640 diff changeset	187	Swing_Thread.now { buffer_lock(buffer) { body } }
d95522496593 more careful locking of jEdit buffer; wenzelm parents: 38640 diff changeset	188
40474 576b88b1dce9 added buffer_text convenience, with explicit locking; wenzelm parents: 39741 diff changeset	189	def buffer_text(buffer: JEditBuffer): String =
576b88b1dce9 added buffer_text convenience, with explicit locking; wenzelm parents: 39741 diff changeset	190	buffer_lock(buffer) { buffer.getText(0, buffer.getLength) }
576b88b1dce9 added buffer_text convenience, with explicit locking; wenzelm parents: 39741 diff changeset	191
44574 24444588fddd actual auto loading of required files; wenzelm parents: 44573 diff changeset	192	def buffer_name(buffer: Buffer): String = buffer.getSymlinkPath
24444588fddd actual auto loading of required files; wenzelm parents: 44573 diff changeset	193
44160 8848867501fb clarified document model header: master_dir (native wrt. editor, potentially URL) and node_name (full canonical path); wenzelm parents: 43714 diff changeset	194	def buffer_path(buffer: Buffer): (String, String) =
44574 24444588fddd actual auto loading of required files; wenzelm parents: 44573 diff changeset	195	(buffer.getDirectory, buffer_name(buffer))
44160 8848867501fb clarified document model header: master_dir (native wrt. editor, potentially URL) and node_name (full canonical path); wenzelm parents: 43714 diff changeset	196
34784 02959dcea756 split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea); wenzelm parents: 34782 diff changeset	197
43449 591598bc52bc convenience functions; wenzelm parents: 43443 diff changeset	198	/* document model and view */
591598bc52bc convenience functions; wenzelm parents: 43443 diff changeset	199
591598bc52bc convenience functions; wenzelm parents: 43443 diff changeset	200	def document_model(buffer: Buffer): Option[Document_Model] = Document_Model(buffer)
591598bc52bc convenience functions; wenzelm parents: 43443 diff changeset	201	def document_view(text_area: JEditTextArea): Option[Document_View] = Document_View(text_area)
591598bc52bc convenience functions; wenzelm parents: 43443 diff changeset	202
44379 1079ab6b342b added official Text.Range.Ordering; wenzelm parents: 44238 diff changeset	203	def document_views(buffer: Buffer): List[Document_View] =
1079ab6b342b added official Text.Range.Ordering; wenzelm parents: 44238 diff changeset	204	for {
1079ab6b342b added official Text.Range.Ordering; wenzelm parents: 44238 diff changeset	205	text_area <- jedit_text_areas(buffer).toList
1079ab6b342b added official Text.Range.Ordering; wenzelm parents: 44238 diff changeset	206	val doc_view = document_view(text_area)
1079ab6b342b added official Text.Range.Ordering; wenzelm parents: 44238 diff changeset	207	if doc_view.isDefined
1079ab6b342b added official Text.Range.Ordering; wenzelm parents: 44238 diff changeset	208	} yield doc_view.get
1079ab6b342b added official Text.Range.Ordering; wenzelm parents: 44238 diff changeset	209
43510 17d431c92575 init/exit model/view synchronously within the swing thread -- EditBus.send in jedit-4.4.1 always runs there; wenzelm parents: 43487 diff changeset	210	def init_model(buffer: Buffer)
17d431c92575 init/exit model/view synchronously within the swing thread -- EditBus.send in jedit-4.4.1 always runs there; wenzelm parents: 43487 diff changeset	211	{
17d431c92575 init/exit model/view synchronously within the swing thread -- EditBus.send in jedit-4.4.1 always runs there; wenzelm parents: 43487 diff changeset	212	swing_buffer_lock(buffer) {
17d431c92575 init/exit model/view synchronously within the swing thread -- EditBus.send in jedit-4.4.1 always runs there; wenzelm parents: 43487 diff changeset	213	val opt_model =
17d431c92575 init/exit model/view synchronously within the swing thread -- EditBus.send in jedit-4.4.1 always runs there; wenzelm parents: 43487 diff changeset	214	document_model(buffer) match {
17d431c92575 init/exit model/view synchronously within the swing thread -- EditBus.send in jedit-4.4.1 always runs there; wenzelm parents: 43487 diff changeset	215	case Some(model) => Some(model)
17d431c92575 init/exit model/view synchronously within the swing thread -- EditBus.send in jedit-4.4.1 always runs there; wenzelm parents: 43487 diff changeset	216	case None =>
44160 8848867501fb clarified document model header: master_dir (native wrt. editor, potentially URL) and node_name (full canonical path); wenzelm parents: 43714 diff changeset	217	val (master_dir, path) = buffer_path(buffer)
8848867501fb clarified document model header: master_dir (native wrt. editor, potentially URL) and node_name (full canonical path); wenzelm parents: 43714 diff changeset	218	Thy_Header.thy_name(path) match {
44222 9d5ef6cd4ee1 use full .thy file name as node name, which makes MiscUtilities.resolveSymlinks/File.getCanonicalPath more predictable; wenzelm parents: 44221 diff changeset	219	case Some(name) =>
9d5ef6cd4ee1 use full .thy file name as node name, which makes MiscUtilities.resolveSymlinks/File.getCanonicalPath more predictable; wenzelm parents: 44221 diff changeset	220	Some(Document_Model.init(session, buffer, master_dir, path, name))
44160 8848867501fb clarified document model header: master_dir (native wrt. editor, potentially URL) and node_name (full canonical path); wenzelm parents: 43714 diff changeset	221	case None => None
43510 17d431c92575 init/exit model/view synchronously within the swing thread -- EditBus.send in jedit-4.4.1 always runs there; wenzelm parents: 43487 diff changeset	222	}
17d431c92575 init/exit model/view synchronously within the swing thread -- EditBus.send in jedit-4.4.1 always runs there; wenzelm parents: 43487 diff changeset	223	}
17d431c92575 init/exit model/view synchronously within the swing thread -- EditBus.send in jedit-4.4.1 always runs there; wenzelm parents: 43487 diff changeset	224	if (opt_model.isDefined) {
17d431c92575 init/exit model/view synchronously within the swing thread -- EditBus.send in jedit-4.4.1 always runs there; wenzelm parents: 43487 diff changeset	225	for (text_area <- jedit_text_areas(buffer)) {
17d431c92575 init/exit model/view synchronously within the swing thread -- EditBus.send in jedit-4.4.1 always runs there; wenzelm parents: 43487 diff changeset	226	if (document_view(text_area).map(_.model) != opt_model)
17d431c92575 init/exit model/view synchronously within the swing thread -- EditBus.send in jedit-4.4.1 always runs there; wenzelm parents: 43487 diff changeset	227	Document_View.init(opt_model.get, text_area)
17d431c92575 init/exit model/view synchronously within the swing thread -- EditBus.send in jedit-4.4.1 always runs there; wenzelm parents: 43487 diff changeset	228	}
17d431c92575 init/exit model/view synchronously within the swing thread -- EditBus.send in jedit-4.4.1 always runs there; wenzelm parents: 43487 diff changeset	229	}
17d431c92575 init/exit model/view synchronously within the swing thread -- EditBus.send in jedit-4.4.1 always runs there; wenzelm parents: 43487 diff changeset	230	}
17d431c92575 init/exit model/view synchronously within the swing thread -- EditBus.send in jedit-4.4.1 always runs there; wenzelm parents: 43487 diff changeset	231	}
17d431c92575 init/exit model/view synchronously within the swing thread -- EditBus.send in jedit-4.4.1 always runs there; wenzelm parents: 43487 diff changeset	232
17d431c92575 init/exit model/view synchronously within the swing thread -- EditBus.send in jedit-4.4.1 always runs there; wenzelm parents: 43487 diff changeset	233	def exit_model(buffer: Buffer)
17d431c92575 init/exit model/view synchronously within the swing thread -- EditBus.send in jedit-4.4.1 always runs there; wenzelm parents: 43487 diff changeset	234	{
17d431c92575 init/exit model/view synchronously within the swing thread -- EditBus.send in jedit-4.4.1 always runs there; wenzelm parents: 43487 diff changeset	235	swing_buffer_lock(buffer) {
17d431c92575 init/exit model/view synchronously within the swing thread -- EditBus.send in jedit-4.4.1 always runs there; wenzelm parents: 43487 diff changeset	236	jedit_text_areas(buffer).foreach(Document_View.exit)
17d431c92575 init/exit model/view synchronously within the swing thread -- EditBus.send in jedit-4.4.1 always runs there; wenzelm parents: 43487 diff changeset	237	Document_Model.exit(buffer)
17d431c92575 init/exit model/view synchronously within the swing thread -- EditBus.send in jedit-4.4.1 always runs there; wenzelm parents: 43487 diff changeset	238	}
17d431c92575 init/exit model/view synchronously within the swing thread -- EditBus.send in jedit-4.4.1 always runs there; wenzelm parents: 43487 diff changeset	239	}
17d431c92575 init/exit model/view synchronously within the swing thread -- EditBus.send in jedit-4.4.1 always runs there; wenzelm parents: 43487 diff changeset	240
17d431c92575 init/exit model/view synchronously within the swing thread -- EditBus.send in jedit-4.4.1 always runs there; wenzelm parents: 43487 diff changeset	241	def init_view(buffer: Buffer, text_area: JEditTextArea)
17d431c92575 init/exit model/view synchronously within the swing thread -- EditBus.send in jedit-4.4.1 always runs there; wenzelm parents: 43487 diff changeset	242	{
17d431c92575 init/exit model/view synchronously within the swing thread -- EditBus.send in jedit-4.4.1 always runs there; wenzelm parents: 43487 diff changeset	243	swing_buffer_lock(buffer) {
17d431c92575 init/exit model/view synchronously within the swing thread -- EditBus.send in jedit-4.4.1 always runs there; wenzelm parents: 43487 diff changeset	244	document_model(buffer) match {
17d431c92575 init/exit model/view synchronously within the swing thread -- EditBus.send in jedit-4.4.1 always runs there; wenzelm parents: 43487 diff changeset	245	case Some(model) => Document_View.init(model, text_area)
17d431c92575 init/exit model/view synchronously within the swing thread -- EditBus.send in jedit-4.4.1 always runs there; wenzelm parents: 43487 diff changeset	246	case None =>
17d431c92575 init/exit model/view synchronously within the swing thread -- EditBus.send in jedit-4.4.1 always runs there; wenzelm parents: 43487 diff changeset	247	}
17d431c92575 init/exit model/view synchronously within the swing thread -- EditBus.send in jedit-4.4.1 always runs there; wenzelm parents: 43487 diff changeset	248	}
17d431c92575 init/exit model/view synchronously within the swing thread -- EditBus.send in jedit-4.4.1 always runs there; wenzelm parents: 43487 diff changeset	249	}
17d431c92575 init/exit model/view synchronously within the swing thread -- EditBus.send in jedit-4.4.1 always runs there; wenzelm parents: 43487 diff changeset	250
17d431c92575 init/exit model/view synchronously within the swing thread -- EditBus.send in jedit-4.4.1 always runs there; wenzelm parents: 43487 diff changeset	251	def exit_view(buffer: Buffer, text_area: JEditTextArea)
17d431c92575 init/exit model/view synchronously within the swing thread -- EditBus.send in jedit-4.4.1 always runs there; wenzelm parents: 43487 diff changeset	252	{
17d431c92575 init/exit model/view synchronously within the swing thread -- EditBus.send in jedit-4.4.1 always runs there; wenzelm parents: 43487 diff changeset	253	swing_buffer_lock(buffer) {
17d431c92575 init/exit model/view synchronously within the swing thread -- EditBus.send in jedit-4.4.1 always runs there; wenzelm parents: 43487 diff changeset	254	Document_View.exit(text_area)
17d431c92575 init/exit model/view synchronously within the swing thread -- EditBus.send in jedit-4.4.1 always runs there; wenzelm parents: 43487 diff changeset	255	}
17d431c92575 init/exit model/view synchronously within the swing thread -- EditBus.send in jedit-4.4.1 always runs there; wenzelm parents: 43487 diff changeset	256	}
17d431c92575 init/exit model/view synchronously within the swing thread -- EditBus.send in jedit-4.4.1 always runs there; wenzelm parents: 43487 diff changeset	257
43449 591598bc52bc convenience functions; wenzelm parents: 43443 diff changeset	258
37068 07936a4efe93 access statically typed dockable windows; wenzelm parents: 37019 diff changeset	259	/* dockable windows */
07936a4efe93 access statically typed dockable windows; wenzelm parents: 37019 diff changeset	260
07936a4efe93 access statically typed dockable windows; wenzelm parents: 37019 diff changeset	261	private def wm(view: View): DockableWindowManager = view.getDockableWindowManager
07936a4efe93 access statically typed dockable windows; wenzelm parents: 37019 diff changeset	262
39515 57ceabb0bb8e basic setup for prover session panel; wenzelm parents: 39241 diff changeset	263	def docked_session(view: View): Option[Session_Dockable] =
57ceabb0bb8e basic setup for prover session panel; wenzelm parents: 39241 diff changeset	264	wm(view).getDockableWindow("isabelle-session") match {
57ceabb0bb8e basic setup for prover session panel; wenzelm parents: 39241 diff changeset	265	case dockable: Session_Dockable => Some(dockable)
57ceabb0bb8e basic setup for prover session panel; wenzelm parents: 39241 diff changeset	266	case _ => None
57ceabb0bb8e basic setup for prover session panel; wenzelm parents: 39241 diff changeset	267	}
57ceabb0bb8e basic setup for prover session panel; wenzelm parents: 39241 diff changeset	268
37068 07936a4efe93 access statically typed dockable windows; wenzelm parents: 37019 diff changeset	269	def docked_output(view: View): Option[Output_Dockable] =
07936a4efe93 access statically typed dockable windows; wenzelm parents: 37019 diff changeset	270	wm(view).getDockableWindow("isabelle-output") match {
07936a4efe93 access statically typed dockable windows; wenzelm parents: 37019 diff changeset	271	case dockable: Output_Dockable => Some(dockable)
07936a4efe93 access statically typed dockable windows; wenzelm parents: 37019 diff changeset	272	case _ => None
07936a4efe93 access statically typed dockable windows; wenzelm parents: 37019 diff changeset	273	}
07936a4efe93 access statically typed dockable windows; wenzelm parents: 37019 diff changeset	274
07936a4efe93 access statically typed dockable windows; wenzelm parents: 37019 diff changeset	275	def docked_raw_output(view: View): Option[Raw_Output_Dockable] =
07936a4efe93 access statically typed dockable windows; wenzelm parents: 37019 diff changeset	276	wm(view).getDockableWindow("isabelle-raw-output") match {
07936a4efe93 access statically typed dockable windows; wenzelm parents: 37019 diff changeset	277	case dockable: Raw_Output_Dockable => Some(dockable)
07936a4efe93 access statically typed dockable windows; wenzelm parents: 37019 diff changeset	278	case _ => None
07936a4efe93 access statically typed dockable windows; wenzelm parents: 37019 diff changeset	279	}
07936a4efe93 access statically typed dockable windows; wenzelm parents: 37019 diff changeset	280
07936a4efe93 access statically typed dockable windows; wenzelm parents: 37019 diff changeset	281	def docked_protocol(view: View): Option[Protocol_Dockable] =
07936a4efe93 access statically typed dockable windows; wenzelm parents: 37019 diff changeset	282	wm(view).getDockableWindow("isabelle-protocol") match {
07936a4efe93 access statically typed dockable windows; wenzelm parents: 37019 diff changeset	283	case dockable: Protocol_Dockable => Some(dockable)
07936a4efe93 access statically typed dockable windows; wenzelm parents: 37019 diff changeset	284	case _ => None
07936a4efe93 access statically typed dockable windows; wenzelm parents: 37019 diff changeset	285	}
07936a4efe93 access statically typed dockable windows; wenzelm parents: 37019 diff changeset	286
07936a4efe93 access statically typed dockable windows; wenzelm parents: 37019 diff changeset	287
39517 e036c67448e6 separate Isabelle.logic_selector; wenzelm parents: 39515 diff changeset	288	/* logic image */
e036c67448e6 separate Isabelle.logic_selector; wenzelm parents: 39515 diff changeset	289
e036c67448e6 separate Isabelle.logic_selector; wenzelm parents: 39515 diff changeset	290	def default_logic(): String =
e036c67448e6 separate Isabelle.logic_selector; wenzelm parents: 39515 diff changeset	291	{
43661 39fdbd814c7f quasi-static Isabelle_System -- reduced tendency towards "functorial style"; wenzelm parents: 43648 diff changeset	292	val logic = Isabelle_System.getenv("JEDIT_LOGIC")
39517 e036c67448e6 separate Isabelle.logic_selector; wenzelm parents: 39515 diff changeset	293	if (logic != "") logic
43661 39fdbd814c7f quasi-static Isabelle_System -- reduced tendency towards "functorial style"; wenzelm parents: 43648 diff changeset	294	else Isabelle_System.getenv_strict("ISABELLE_LOGIC")
39517 e036c67448e6 separate Isabelle.logic_selector; wenzelm parents: 39515 diff changeset	295	}
e036c67448e6 separate Isabelle.logic_selector; wenzelm parents: 39515 diff changeset	296
e036c67448e6 separate Isabelle.logic_selector; wenzelm parents: 39515 diff changeset	297	class Logic_Entry(val name: String, val description: String)
e036c67448e6 separate Isabelle.logic_selector; wenzelm parents: 39515 diff changeset	298	{
e036c67448e6 separate Isabelle.logic_selector; wenzelm parents: 39515 diff changeset	299	override def toString = description
e036c67448e6 separate Isabelle.logic_selector; wenzelm parents: 39515 diff changeset	300	}
e036c67448e6 separate Isabelle.logic_selector; wenzelm parents: 39515 diff changeset	301
e036c67448e6 separate Isabelle.logic_selector; wenzelm parents: 39515 diff changeset	302	def logic_selector(logic: String): ComboBox[Logic_Entry] =
e036c67448e6 separate Isabelle.logic_selector; wenzelm parents: 39515 diff changeset	303	{
e036c67448e6 separate Isabelle.logic_selector; wenzelm parents: 39515 diff changeset	304	val entries =
e036c67448e6 separate Isabelle.logic_selector; wenzelm parents: 39515 diff changeset	305	new Logic_Entry("", "default (" + default_logic() + ")") ::
43661 39fdbd814c7f quasi-static Isabelle_System -- reduced tendency towards "functorial style"; wenzelm parents: 43648 diff changeset	306	Isabelle_System.find_logics().map(name => new Logic_Entry(name, name))
39517 e036c67448e6 separate Isabelle.logic_selector; wenzelm parents: 39515 diff changeset	307	val component = new ComboBox(entries)
e036c67448e6 separate Isabelle.logic_selector; wenzelm parents: 39515 diff changeset	308	entries.find(_.name == logic) match {
e036c67448e6 separate Isabelle.logic_selector; wenzelm parents: 39515 diff changeset	309	case None =>
e036c67448e6 separate Isabelle.logic_selector; wenzelm parents: 39515 diff changeset	310	case Some(entry) => component.selection.item = entry
e036c67448e6 separate Isabelle.logic_selector; wenzelm parents: 39515 diff changeset	311	}
39702 d7c256cb2797 Session_Dockable: more startup controls; wenzelm parents: 39701 diff changeset	312	component.tooltip = "Isabelle logic image"
39517 e036c67448e6 separate Isabelle.logic_selector; wenzelm parents: 39515 diff changeset	313	component
e036c67448e6 separate Isabelle.logic_selector; wenzelm parents: 39515 diff changeset	314	}
39702 d7c256cb2797 Session_Dockable: more startup controls; wenzelm parents: 39701 diff changeset	315
d7c256cb2797 Session_Dockable: more startup controls; wenzelm parents: 39701 diff changeset	316	def start_session()
d7c256cb2797 Session_Dockable: more startup controls; wenzelm parents: 39701 diff changeset	317	{
40852 aee98c88c587 builtin time bounds (again); wenzelm parents: 40850 diff changeset	318	val timeout = Time_Property("startup-timeout", Time.seconds(10)) max Time.seconds(5)
43670 7f933761764b prefer space_explode/split_lines as in Isabelle/ML; wenzelm parents: 43661 diff changeset	319	val modes = space_explode(',', Isabelle_System.getenv("JEDIT_PRINT_MODE")).map("-m" + _)
39702 d7c256cb2797 Session_Dockable: more startup controls; wenzelm parents: 39701 diff changeset	320	val logic = {
d7c256cb2797 Session_Dockable: more startup controls; wenzelm parents: 39701 diff changeset	321	val logic = Property("logic")
d7c256cb2797 Session_Dockable: more startup controls; wenzelm parents: 39701 diff changeset	322	if (logic != null && logic != "") logic
d7c256cb2797 Session_Dockable: more startup controls; wenzelm parents: 39701 diff changeset	323	else Isabelle.default_logic()
d7c256cb2797 Session_Dockable: more startup controls; wenzelm parents: 39701 diff changeset	324	}
40850 d804de9ac970 more abstract handling of Time properties; wenzelm parents: 40849 diff changeset	325	session.start(timeout, modes ::: List(logic))
39702 d7c256cb2797 Session_Dockable: more startup controls; wenzelm parents: 39701 diff changeset	326	}
44238 36120feb70ed some convenience actions/shortcuts for control symbols; wenzelm parents: 44225 diff changeset	327
36120feb70ed some convenience actions/shortcuts for control symbols; wenzelm parents: 44225 diff changeset	328
36120feb70ed some convenience actions/shortcuts for control symbols; wenzelm parents: 44225 diff changeset	329	/* convenience actions */
36120feb70ed some convenience actions/shortcuts for control symbols; wenzelm parents: 44225 diff changeset	330
36120feb70ed some convenience actions/shortcuts for control symbols; wenzelm parents: 44225 diff changeset	331	private def user_input(text_area: JEditTextArea, s1: String, s2: String = "")
36120feb70ed some convenience actions/shortcuts for control symbols; wenzelm parents: 44225 diff changeset	332	{
36120feb70ed some convenience actions/shortcuts for control symbols; wenzelm parents: 44225 diff changeset	333	s1.foreach(text_area.userInput(_))
36120feb70ed some convenience actions/shortcuts for control symbols; wenzelm parents: 44225 diff changeset	334	s2.foreach(text_area.userInput(_))
36120feb70ed some convenience actions/shortcuts for control symbols; wenzelm parents: 44225 diff changeset	335	s2.foreach(_ => text_area.goToPrevCharacter(false))
36120feb70ed some convenience actions/shortcuts for control symbols; wenzelm parents: 44225 diff changeset	336	}
36120feb70ed some convenience actions/shortcuts for control symbols; wenzelm parents: 44225 diff changeset	337
36120feb70ed some convenience actions/shortcuts for control symbols; wenzelm parents: 44225 diff changeset	338	def input_sub(text_area: JEditTextArea): Unit = user_input(text_area, Symbol.sub_decoded)
36120feb70ed some convenience actions/shortcuts for control symbols; wenzelm parents: 44225 diff changeset	339	def input_sup(text_area: JEditTextArea): Unit = user_input(text_area, Symbol.sup_decoded)
36120feb70ed some convenience actions/shortcuts for control symbols; wenzelm parents: 44225 diff changeset	340	def input_isub(text_area: JEditTextArea): Unit = user_input(text_area, Symbol.isub_decoded)
36120feb70ed some convenience actions/shortcuts for control symbols; wenzelm parents: 44225 diff changeset	341	def input_isup(text_area: JEditTextArea): Unit = user_input(text_area, Symbol.isup_decoded)
36120feb70ed some convenience actions/shortcuts for control symbols; wenzelm parents: 44225 diff changeset	342	def input_bsub(text_area: JEditTextArea): Unit = user_input(text_area, Symbol.bsub_decoded, Symbol.esub_decoded)
36120feb70ed some convenience actions/shortcuts for control symbols; wenzelm parents: 44225 diff changeset	343	def input_bsup(text_area: JEditTextArea): Unit = user_input(text_area, Symbol.bsup_decoded, Symbol.esup_decoded)
36120feb70ed some convenience actions/shortcuts for control symbols; wenzelm parents: 44225 diff changeset	344	def input_bold(text_area: JEditTextArea): Unit = user_input(text_area, Symbol.bold_decoded)
34318 c13e168a8ae6 original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout; wenzelm parents: diff changeset	345	}
c13e168a8ae6 original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout; wenzelm parents: diff changeset	346
34429 03afc73e185f tuned; wenzelm parents: 34422 diff changeset	347
34618 e45052ff7233 added Boolean_Property, Int_Property; wenzelm parents: 34615 diff changeset	348	class Plugin extends EBPlugin
e45052ff7233 added Boolean_Property, Int_Property; wenzelm parents: 34615 diff changeset	349	{
44574 24444588fddd actual auto loading of required files; wenzelm parents: 44573 diff changeset	350	/* theory files via editor document model */
24444588fddd actual auto loading of required files; wenzelm parents: 44573 diff changeset	351
24444588fddd actual auto loading of required files; wenzelm parents: 44573 diff changeset	352	val thy_load = new Thy_Load
24444588fddd actual auto loading of required files; wenzelm parents: 44573 diff changeset	353	{
24444588fddd actual auto loading of required files; wenzelm parents: 44573 diff changeset	354	private var loaded_theories: Set[String] = Set()
43645 ac886d096c11 some support for Session.File_Store; wenzelm parents: 43643 diff changeset	355
44574 24444588fddd actual auto loading of required files; wenzelm parents: 44573 diff changeset	356	def register_thy(thy_name: String)
24444588fddd actual auto loading of required files; wenzelm parents: 44573 diff changeset	357	{
24444588fddd actual auto loading of required files; wenzelm parents: 44573 diff changeset	358	synchronized { loaded_theories += thy_name }
24444588fddd actual auto loading of required files; wenzelm parents: 44573 diff changeset	359	}
24444588fddd actual auto loading of required files; wenzelm parents: 44573 diff changeset	360	def is_loaded(thy_name: String): Boolean =
24444588fddd actual auto loading of required files; wenzelm parents: 44573 diff changeset	361	synchronized { loaded_theories.contains(thy_name) }
24444588fddd actual auto loading of required files; wenzelm parents: 44573 diff changeset	362
44185 05641edb5d30 provide node header via Scala layer; wenzelm parents: 44163 diff changeset	363	def append(master_dir: String, source_path: Path): String =
43645 ac886d096c11 some support for Session.File_Store; wenzelm parents: 43643 diff changeset	364	{
44185 05641edb5d30 provide node header via Scala layer; wenzelm parents: 44163 diff changeset	365	val path = source_path.expand
05641edb5d30 provide node header via Scala layer; wenzelm parents: 44163 diff changeset	366	if (path.is_absolute) Isabelle_System.platform_path(path)
05641edb5d30 provide node header via Scala layer; wenzelm parents: 44163 diff changeset	367	else {
05641edb5d30 provide node header via Scala layer; wenzelm parents: 44163 diff changeset	368	val vfs = VFSManager.getVFSForPath(master_dir)
05641edb5d30 provide node header via Scala layer; wenzelm parents: 44163 diff changeset	369	if (vfs.isInstanceOf[FileVFS])
44222 9d5ef6cd4ee1 use full .thy file name as node name, which makes MiscUtilities.resolveSymlinks/File.getCanonicalPath more predictable; wenzelm parents: 44221 diff changeset	370	MiscUtilities.resolveSymlinks(
9d5ef6cd4ee1 use full .thy file name as node name, which makes MiscUtilities.resolveSymlinks/File.getCanonicalPath more predictable; wenzelm parents: 44221 diff changeset	371	vfs.constructPath(master_dir, Isabelle_System.platform_path(path)))
44185 05641edb5d30 provide node header via Scala layer; wenzelm parents: 44163 diff changeset	372	else vfs.constructPath(master_dir, Isabelle_System.standard_path(path))
05641edb5d30 provide node header via Scala layer; wenzelm parents: 44163 diff changeset	373	}
44163 32e0c150c010 normalized theory dependencies wrt. file_store; wenzelm parents: 44160 diff changeset	374	}
43645 ac886d096c11 some support for Session.File_Store; wenzelm parents: 43643 diff changeset	375
44574 24444588fddd actual auto loading of required files; wenzelm parents: 44573 diff changeset	376	def check_thy(node_name: String): Thy_Header =
44163 32e0c150c010 normalized theory dependencies wrt. file_store; wenzelm parents: 44160 diff changeset	377	{
44574 24444588fddd actual auto loading of required files; wenzelm parents: 44573 diff changeset	378	Swing_Thread.now {
24444588fddd actual auto loading of required files; wenzelm parents: 44573 diff changeset	379	Isabelle.jedit_buffers().find(buffer => Isabelle.buffer_name(buffer) == node_name) match {
24444588fddd actual auto loading of required files; wenzelm parents: 44573 diff changeset	380	case Some(buffer) =>
24444588fddd actual auto loading of required files; wenzelm parents: 44573 diff changeset	381	Isabelle.buffer_lock(buffer) {
24444588fddd actual auto loading of required files; wenzelm parents: 44573 diff changeset	382	val text = new Segment
24444588fddd actual auto loading of required files; wenzelm parents: 44573 diff changeset	383	buffer.getText(0, buffer.getLength, text)
24444588fddd actual auto loading of required files; wenzelm parents: 44573 diff changeset	384	Some(Thy_Header.read(text))
24444588fddd actual auto loading of required files; wenzelm parents: 44573 diff changeset	385	}
24444588fddd actual auto loading of required files; wenzelm parents: 44573 diff changeset	386	case None => None
24444588fddd actual auto loading of required files; wenzelm parents: 44573 diff changeset	387	}
24444588fddd actual auto loading of required files; wenzelm parents: 44573 diff changeset	388	} getOrElse {
24444588fddd actual auto loading of required files; wenzelm parents: 44573 diff changeset	389	val file = new File(node_name) // FIXME load URL via jEdit VFS (!?)
24444588fddd actual auto loading of required files; wenzelm parents: 44573 diff changeset	390	if (!file.exists \|\| !file.isFile) error("No such file: " + quote(file.toString))
24444588fddd actual auto loading of required files; wenzelm parents: 44573 diff changeset	391	Thy_Header.read(file)
43645 ac886d096c11 some support for Session.File_Store; wenzelm parents: 43643 diff changeset	392	}
ac886d096c11 some support for Session.File_Store; wenzelm parents: 43643 diff changeset	393	}
ac886d096c11 some support for Session.File_Store; wenzelm parents: 43643 diff changeset	394	}
ac886d096c11 some support for Session.File_Store; wenzelm parents: 43643 diff changeset	395
44574 24444588fddd actual auto loading of required files; wenzelm parents: 44573 diff changeset	396	val thy_info = new Thy_Info(thy_load)
39630 44181423183a explicit Session.Phase indication with associated event bus; wenzelm parents: 39628 diff changeset	397
44573 51f8895b9ad9 some dialog for auto loading of required files (still inactive); wenzelm parents: 44434 diff changeset	398	private lazy val delay_load =
44574 24444588fddd actual auto loading of required files; wenzelm parents: 44573 diff changeset	399	Swing_Thread.delay_last(Isabelle.session.load_delay)
24444588fddd actual auto loading of required files; wenzelm parents: 44573 diff changeset	400	{
24444588fddd actual auto loading of required files; wenzelm parents: 44573 diff changeset	401	val buffers = Isabelle.jedit_buffers().toList
24444588fddd actual auto loading of required files; wenzelm parents: 44573 diff changeset	402	def loaded_buffer(name: String): Boolean =
24444588fddd actual auto loading of required files; wenzelm parents: 44573 diff changeset	403	buffers.exists(buffer => Isabelle.buffer_name(buffer) == name)
24444588fddd actual auto loading of required files; wenzelm parents: 44573 diff changeset	404
24444588fddd actual auto loading of required files; wenzelm parents: 44573 diff changeset	405	val thys =
24444588fddd actual auto loading of required files; wenzelm parents: 44573 diff changeset	406	for (buffer <- buffers; model <- Isabelle.document_model(buffer))
24444588fddd actual auto loading of required files; wenzelm parents: 44573 diff changeset	407	yield (model.master_dir, model.thy_name)
24444588fddd actual auto loading of required files; wenzelm parents: 44573 diff changeset	408	val files = thy_info.dependencies(thys).map(_._1).filterNot(loaded_buffer _)
24444588fddd actual auto loading of required files; wenzelm parents: 44573 diff changeset	409
24444588fddd actual auto loading of required files; wenzelm parents: 44573 diff changeset	410	val do_load = !files.isEmpty &&
44573 51f8895b9ad9 some dialog for auto loading of required files (still inactive); wenzelm parents: 44434 diff changeset	411	{
44574 24444588fddd actual auto loading of required files; wenzelm parents: 44573 diff changeset	412	val files_sorted = { val a = files.toArray; Sorting.quickSort(a); a.toList }
24444588fddd actual auto loading of required files; wenzelm parents: 44573 diff changeset	413	val files_text = new scala.swing.TextArea(files_sorted.mkString("\n"))
24444588fddd actual auto loading of required files; wenzelm parents: 44573 diff changeset	414	files_text.editable = false
24444588fddd actual auto loading of required files; wenzelm parents: 44573 diff changeset	415	Library.confirm_dialog(jEdit.getActiveView(),
44573 51f8895b9ad9 some dialog for auto loading of required files (still inactive); wenzelm parents: 44434 diff changeset	416	"Auto loading of required files",
51f8895b9ad9 some dialog for auto loading of required files (still inactive); wenzelm parents: 44434 diff changeset	417	JOptionPane.YES_NO_OPTION,
44574 24444588fddd actual auto loading of required files; wenzelm parents: 44573 diff changeset	418	"The following files are required to resolve theory imports. Reload now?",
24444588fddd actual auto loading of required files; wenzelm parents: 44573 diff changeset	419	files_text) == 0
44573 51f8895b9ad9 some dialog for auto loading of required files (still inactive); wenzelm parents: 44434 diff changeset	420	}
44574 24444588fddd actual auto loading of required files; wenzelm parents: 44573 diff changeset	421	if (do_load)
24444588fddd actual auto loading of required files; wenzelm parents: 44573 diff changeset	422	for (file <- files if !loaded_buffer(file))
24444588fddd actual auto loading of required files; wenzelm parents: 44573 diff changeset	423	jEdit.openFile(null: View, file)
24444588fddd actual auto loading of required files; wenzelm parents: 44573 diff changeset	424	}
44573 51f8895b9ad9 some dialog for auto loading of required files (still inactive); wenzelm parents: 44434 diff changeset	425
44574 24444588fddd actual auto loading of required files; wenzelm parents: 44573 diff changeset	426
24444588fddd actual auto loading of required files; wenzelm parents: 44573 diff changeset	427	/* session manager */
44573 51f8895b9ad9 some dialog for auto loading of required files (still inactive); wenzelm parents: 44434 diff changeset	428
39633 26a28110ece5 simplified Session.Phase; wenzelm parents: 39631 diff changeset	429	private val session_manager = actor {
26a28110ece5 simplified Session.Phase; wenzelm parents: 39631 diff changeset	430	loop {
26a28110ece5 simplified Session.Phase; wenzelm parents: 39631 diff changeset	431	react {
39735 969ede84aac0 more uniform init/exit model/view in session_manager, trading race wrt. session.phase for race wrt. global editor state; wenzelm parents: 39702 diff changeset	432	case phase: Session.Phase =>
969ede84aac0 more uniform init/exit model/view in session_manager, trading race wrt. session.phase for race wrt. global editor state; wenzelm parents: 39702 diff changeset	433	phase match {
969ede84aac0 more uniform init/exit model/view in session_manager, trading race wrt. session.phase for race wrt. global editor state; wenzelm parents: 39702 diff changeset	434	case Session.Failed =>
969ede84aac0 more uniform init/exit model/view in session_manager, trading race wrt. session.phase for race wrt. global editor state; wenzelm parents: 39702 diff changeset	435	Swing_Thread.now {
969ede84aac0 more uniform init/exit model/view in session_manager, trading race wrt. session.phase for race wrt. global editor state; wenzelm parents: 39702 diff changeset	436	val text = new scala.swing.TextArea(Isabelle.session.syslog())
969ede84aac0 more uniform init/exit model/view in session_manager, trading race wrt. session.phase for race wrt. global editor state; wenzelm parents: 39702 diff changeset	437	text.editable = false
969ede84aac0 more uniform init/exit model/view in session_manager, trading race wrt. session.phase for race wrt. global editor state; wenzelm parents: 39702 diff changeset	438	Library.error_dialog(jEdit.getActiveView, "Failed to start Isabelle process", text)
969ede84aac0 more uniform init/exit model/view in session_manager, trading race wrt. session.phase for race wrt. global editor state; wenzelm parents: 39702 diff changeset	439	}
969ede84aac0 more uniform init/exit model/view in session_manager, trading race wrt. session.phase for race wrt. global editor state; wenzelm parents: 39702 diff changeset	440
44573 51f8895b9ad9 some dialog for auto loading of required files (still inactive); wenzelm parents: 44434 diff changeset	441	case Session.Ready =>
51f8895b9ad9 some dialog for auto loading of required files (still inactive); wenzelm parents: 44434 diff changeset	442	Isabelle.jedit_buffers.foreach(Isabelle.init_model)
51f8895b9ad9 some dialog for auto loading of required files (still inactive); wenzelm parents: 44434 diff changeset	443	delay_load()
51f8895b9ad9 some dialog for auto loading of required files (still inactive); wenzelm parents: 44434 diff changeset	444
43510 17d431c92575 init/exit model/view synchronously within the swing thread -- EditBus.send in jedit-4.4.1 always runs there; wenzelm parents: 43487 diff changeset	445	case Session.Shutdown => Isabelle.jedit_buffers.foreach(Isabelle.exit_model)
39735 969ede84aac0 more uniform init/exit model/view in session_manager, trading race wrt. session.phase for race wrt. global editor state; wenzelm parents: 39702 diff changeset	446	case _ =>
969ede84aac0 more uniform init/exit model/view in session_manager, trading race wrt. session.phase for race wrt. global editor state; wenzelm parents: 39702 diff changeset	447	}
969ede84aac0 more uniform init/exit model/view in session_manager, trading race wrt. session.phase for race wrt. global editor state; wenzelm parents: 39702 diff changeset	448	case bad => System.err.println("session_manager: ignoring bad message " + bad)
39630 44181423183a explicit Session.Phase indication with associated event bus; wenzelm parents: 39628 diff changeset	449	}
44181423183a explicit Session.Phase indication with associated event bus; wenzelm parents: 39628 diff changeset	450	}
44181423183a explicit Session.Phase indication with associated event bus; wenzelm parents: 39628 diff changeset	451	}
44181423183a explicit Session.Phase indication with associated event bus; wenzelm parents: 39628 diff changeset	452
44181423183a explicit Session.Phase indication with associated event bus; wenzelm parents: 39628 diff changeset	453
34618 e45052ff7233 added Boolean_Property, Int_Property; wenzelm parents: 34615 diff changeset	454	/* main plugin plumbing */
34433 3da749b53842 renamed Plugin.plugin to Plugin.self; wenzelm parents: 34429 diff changeset	455
34767 8dd19c5f8c56 added properties_changed event bus; wenzelm parents: 34764 diff changeset	456	override def handleMessage(message: EBMessage)
34618 e45052ff7233 added Boolean_Property, Int_Property; wenzelm parents: 34615 diff changeset	457	{
43510 17d431c92575 init/exit model/view synchronously within the swing thread -- EditBus.send in jedit-4.4.1 always runs there; wenzelm parents: 43487 diff changeset	458	Swing_Thread.assert()
34767 8dd19c5f8c56 added properties_changed event bus; wenzelm parents: 34764 diff changeset	459	message match {
41383 514bb82514df check JVM later, to avoid potential conflict with jEdit splash screen; wenzelm parents: 41382 diff changeset	460	case msg: EditorStarted =>
43510 17d431c92575 init/exit model/view synchronously within the swing thread -- EditBus.send in jedit-4.4.1 always runs there; wenzelm parents: 43487 diff changeset	461	Isabelle.check_jvm()
17d431c92575 init/exit model/view synchronously within the swing thread -- EditBus.send in jedit-4.4.1 always runs there; wenzelm parents: 43487 diff changeset	462	if (Isabelle.Boolean_Property("auto-start"))
17d431c92575 init/exit model/view synchronously within the swing thread -- EditBus.send in jedit-4.4.1 always runs there; wenzelm parents: 43487 diff changeset	463	Isabelle.start_session()
39630 44181423183a explicit Session.Phase indication with associated event bus; wenzelm parents: 39628 diff changeset	464
37557 1ae272fd4082 refresh Isabelle token marker after buffer properties changed, e.g. when fold mode is switched; wenzelm parents: 37241 diff changeset	465	case msg: BufferUpdate
44434 3b9b684bfa6f handle potentially more approriate BufferUpdate.LOADED event; wenzelm parents: 44379 diff changeset	466	if msg.getWhat == BufferUpdate.LOADED =>
44573 51f8895b9ad9 some dialog for auto loading of required files (still inactive); wenzelm parents: 44434 diff changeset	467	if (Isabelle.session.is_ready) {
51f8895b9ad9 some dialog for auto loading of required files (still inactive); wenzelm parents: 44434 diff changeset	468	val buffer = msg.getBuffer
51f8895b9ad9 some dialog for auto loading of required files (still inactive); wenzelm parents: 44434 diff changeset	469	if (buffer != null) Isabelle.init_model(buffer)
51f8895b9ad9 some dialog for auto loading of required files (still inactive); wenzelm parents: 44434 diff changeset	470	delay_load()
51f8895b9ad9 some dialog for auto loading of required files (still inactive); wenzelm parents: 44434 diff changeset	471	}
37557 1ae272fd4082 refresh Isabelle token marker after buffer properties changed, e.g. when fold mode is switched; wenzelm parents: 37241 diff changeset	472
39634 4030a9ef9c5a separate Plugin.init_model; wenzelm parents: 39633 diff changeset	473	case msg: EditPaneUpdate
39735 969ede84aac0 more uniform init/exit model/view in session_manager, trading race wrt. session.phase for race wrt. global editor state; wenzelm parents: 39702 diff changeset	474	if (msg.getWhat == EditPaneUpdate.BUFFER_CHANGING \|\|
39637 cc3452317b5f slightly more robust EditBus plumbing wrt. Document_View/Document_Model; wenzelm parents: 39634 diff changeset	475	msg.getWhat == EditPaneUpdate.BUFFER_CHANGED \|\|
39634 4030a9ef9c5a separate Plugin.init_model; wenzelm parents: 39633 diff changeset	476	msg.getWhat == EditPaneUpdate.CREATED \|\|
4030a9ef9c5a separate Plugin.init_model; wenzelm parents: 39633 diff changeset	477	msg.getWhat == EditPaneUpdate.DESTROYED) =>
34784 02959dcea756 split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea); wenzelm parents: 34782 diff changeset	478	val edit_pane = msg.getEditPane
02959dcea756 split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea); wenzelm parents: 34782 diff changeset	479	val buffer = edit_pane.getBuffer
02959dcea756 split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea); wenzelm parents: 34782 diff changeset	480	val text_area = edit_pane.getTextArea
02959dcea756 split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea); wenzelm parents: 34782 diff changeset	481
39637 cc3452317b5f slightly more robust EditBus plumbing wrt. Document_View/Document_Model; wenzelm parents: 39634 diff changeset	482	if (buffer != null && text_area != null) {
39735 969ede84aac0 more uniform init/exit model/view in session_manager, trading race wrt. session.phase for race wrt. global editor state; wenzelm parents: 39702 diff changeset	483	if (msg.getWhat == EditPaneUpdate.BUFFER_CHANGED \|\|
43510 17d431c92575 init/exit model/view synchronously within the swing thread -- EditBus.send in jedit-4.4.1 always runs there; wenzelm parents: 43487 diff changeset	484	msg.getWhat == EditPaneUpdate.CREATED) {
43643 474745a899ea eliminated redundant session_ready; wenzelm parents: 43520 diff changeset	485	if (Isabelle.session.is_ready)
43510 17d431c92575 init/exit model/view synchronously within the swing thread -- EditBus.send in jedit-4.4.1 always runs there; wenzelm parents: 43487 diff changeset	486	Isabelle.init_view(buffer, text_area)
17d431c92575 init/exit model/view synchronously within the swing thread -- EditBus.send in jedit-4.4.1 always runs there; wenzelm parents: 43487 diff changeset	487	}
17d431c92575 init/exit model/view synchronously within the swing thread -- EditBus.send in jedit-4.4.1 always runs there; wenzelm parents: 43487 diff changeset	488	else Isabelle.exit_view(buffer, text_area)
34671 d179fcb04cbc output_info specific to prover immler@in.tum.de parents: 34670 diff changeset	489	}
34784 02959dcea756 split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea); wenzelm parents: 34782 diff changeset	490
34777 91d6089cef88 class Session models full session, with or without prover process (cf. heaps, browser_info); wenzelm parents: 34774 diff changeset	491	case msg: PropertiesChanged =>
43390 7ee98a3802af builtin sub/superscript styles for jedit-4.3.2; wenzelm parents: 43282 diff changeset	492	Swing_Thread.now { Isabelle.setup_tooltips() }
34791 b97d5b38dea4 explicit object Session.Global_Settings; wenzelm parents: 34788 diff changeset	493	Isabelle.session.global_settings.event(Session.Global_Settings)
34784 02959dcea756 split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea); wenzelm parents: 34782 diff changeset	494
34318 c13e168a8ae6 original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout; wenzelm parents: diff changeset	495	case _ =>
c13e168a8ae6 original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout; wenzelm parents: diff changeset	496	}
c13e168a8ae6 original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout; wenzelm parents: diff changeset	497	}
c13e168a8ae6 original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout; wenzelm parents: diff changeset	498
34618 e45052ff7233 added Boolean_Property, Int_Property; wenzelm parents: 34615 diff changeset	499	override def start()
e45052ff7233 added Boolean_Property, Int_Property; wenzelm parents: 34615 diff changeset	500	{
43443 5d9693c2337e basic support for extended syntax styles: sub/superscript; wenzelm parents: 43390 diff changeset	501	Isabelle.plugin = this
39630 44181423183a explicit Session.Phase indication with associated event bus; wenzelm parents: 39628 diff changeset	502	Isabelle.setup_tooltips()
43661 39fdbd814c7f quasi-static Isabelle_System -- reduced tendency towards "functorial style"; wenzelm parents: 43648 diff changeset	503	Isabelle_System.init()
39fdbd814c7f quasi-static Isabelle_System -- reduced tendency towards "functorial style"; wenzelm parents: 43648 diff changeset	504	Isabelle_System.install_fonts()
44574 24444588fddd actual auto loading of required files; wenzelm parents: 44573 diff changeset	505	Isabelle.session = new Session(thy_load)
43661 39fdbd814c7f quasi-static Isabelle_System -- reduced tendency towards "functorial style"; wenzelm parents: 43648 diff changeset	506	SyntaxUtilities.setStyleExtender(new Token_Markup.Style_Extender)
43513 06951ddfc812 clarified plugin start/stop; wenzelm parents: 43510 diff changeset	507	if (ModeProvider.instance.isInstanceOf[ModeProvider])
06951ddfc812 clarified plugin start/stop; wenzelm parents: 43510 diff changeset	508	ModeProvider.instance = new Token_Markup.Mode_Provider(ModeProvider.instance)
39633 26a28110ece5 simplified Session.Phase; wenzelm parents: 39631 diff changeset	509	Isabelle.session.phase_changed += session_manager
34318 c13e168a8ae6 original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout; wenzelm parents: diff changeset	510	}
34618 e45052ff7233 added Boolean_Property, Int_Property; wenzelm parents: 34615 diff changeset	511
39628 f6e82967b5cd Plugin.stop: refrain from invalidating Isabelle.session -- some actors/dockables out there might still refer to it; wenzelm parents: 39518 diff changeset	512	override def stop()
34618 e45052ff7233 added Boolean_Property, Int_Property; wenzelm parents: 34615 diff changeset	513	{
43513 06951ddfc812 clarified plugin start/stop; wenzelm parents: 43510 diff changeset	514	Isabelle.session.phase_changed -= session_manager
06951ddfc812 clarified plugin start/stop; wenzelm parents: 43510 diff changeset	515	Isabelle.jedit_buffers.foreach(Isabelle.exit_model)
39628 f6e82967b5cd Plugin.stop: refrain from invalidating Isabelle.session -- some actors/dockables out there might still refer to it; wenzelm parents: 39518 diff changeset	516	Isabelle.session.stop()
34318 c13e168a8ae6 original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout; wenzelm parents: diff changeset	517	}
c13e168a8ae6 original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout; wenzelm parents: diff changeset	518	}

author	wenzelm
	Mon, 29 Aug 2011 21:55:49 +0200
changeset 44574	24444588fddd
parent 44573	51f8895b9ad9
child 44577	96b6388d06c4
permissions	-rw-r--r--