isabelle: src/Tools/jEdit/src/plugin.scala@cb70157293c0 (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
34318 c13e168a8ae6 original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout; wenzelm parents: diff changeset	13	import java.awt.Font
44573 51f8895b9ad9 some dialog for auto loading of required files (still inactive); wenzelm parents: 44434 diff changeset	14	import javax.swing.JOptionPane
34318 c13e168a8ae6 original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout; wenzelm parents: diff changeset	15
34497 184fda8cce04 more explicit indication of mutable collections; wenzelm parents: 34487 diff changeset	16	import scala.collection.mutable
44606 b625650aa2db improved auto loading: selectable file list; wenzelm parents: 44580 diff changeset	17	import scala.swing.{ComboBox, ListView, ScrollPane}
34406 f81cd75ae331 restructured: independent provers in different buffers immler@in.tum.de parents: 34337 diff changeset	18
39241 e9a442606db3 Isabelle.load_icon with some sanity checks; wenzelm parents: 39167 diff changeset	19	import org.gjt.sp.jedit.{jEdit, GUIUtilities, EBMessage, EBPlugin,
44577 96b6388d06c4 separate module for jEdit primitives for loading theory files; wenzelm parents: 44574 diff changeset	20	Buffer, EditPane, ServiceManager, View}
34406 f81cd75ae331 restructured: independent provers in different buffers immler@in.tum.de parents: 34337 diff changeset	21	import org.gjt.sp.jedit.buffer.JEditBuffer
39043 a0d7e9b580ec added gfx_range convenience; wenzelm parents: 38854 diff changeset	22	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	23	import org.gjt.sp.jedit.syntax.{Token => JEditToken, ModeProvider}
49100 e7aecf2a5fc4 prefer old startup dialog scheme (cf. 514bb82514df); wenzelm parents: 49099 diff changeset	24	import org.gjt.sp.jedit.msg.{EditorStarted, BufferUpdate, EditPaneUpdate, PropertiesChanged}
37068 07936a4efe93 access statically typed dockable windows; wenzelm parents: 37019 diff changeset	25	import org.gjt.sp.jedit.gui.DockableWindowManager
34429 03afc73e185f tuned; wenzelm parents: 34422 diff changeset	26
43443 5d9693c2337e basic support for extended syntax styles: sub/superscript; wenzelm parents: 43390 diff changeset	27	import org.gjt.sp.util.SyntaxUtilities
39241 e9a442606db3 Isabelle.load_icon with some sanity checks; wenzelm parents: 39167 diff changeset	28	import org.gjt.sp.util.Log
e9a442606db3 Isabelle.load_icon with some sanity checks; wenzelm parents: 39167 diff changeset	29
44721 ba478c3f7255 tuned imports; wenzelm parents: 44699 diff changeset	30	import scala.actors.Actor._
39630 44181423183a explicit Session.Phase indication with associated event bus; wenzelm parents: 39628 diff changeset	31
34318 c13e168a8ae6 original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout; wenzelm parents: diff changeset	32
34618 e45052ff7233 added Boolean_Property, Int_Property; wenzelm parents: 34615 diff changeset	33	object Isabelle
e45052ff7233 added Boolean_Property, Int_Property; wenzelm parents: 34615 diff changeset	34	{
34784 02959dcea756 split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea); wenzelm parents: 34782 diff changeset	35	/* plugin instance */
02959dcea756 split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea); wenzelm parents: 34782 diff changeset	36
49245 cb70157293c0 manage Isabelle/jEdit options as Isabelle/Scala options (with persistent preferences); wenzelm parents: 49195 diff changeset	37	val options = new JEdit_Options
cb70157293c0 manage Isabelle/jEdit options as Isabelle/Scala options (with persistent preferences); wenzelm parents: 49195 diff changeset	38
49099 10e899bb6530 more permissive handling of plugin startup failure; wenzelm parents: 49098 diff changeset	39	@volatile var startup_failure: Option[Throwable] = None
10e899bb6530 more permissive handling of plugin startup failure; wenzelm parents: 49098 diff changeset	40	@volatile var startup_notified = false
34784 02959dcea756 split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea); wenzelm parents: 34782 diff changeset	41
49101 21c8d2070be9 continue with more robust dummy session after failed startup; wenzelm parents: 49100 diff changeset	42	@volatile var plugin: Plugin = null
21c8d2070be9 continue with more robust dummy session after failed startup; wenzelm parents: 49100 diff changeset	43	@volatile var session: Session = new Session(new JEdit_Thy_Load(Set.empty, Outer_Syntax.empty))
21c8d2070be9 continue with more robust dummy session after failed startup; wenzelm parents: 49100 diff changeset	44
48870 4accee106f0f clarified initialization of Thy_Load, Thy_Info, Session; wenzelm parents: 48791 diff changeset	45	def thy_load(): JEdit_Thy_Load =
4accee106f0f clarified initialization of Thy_Load, Thy_Info, Session; wenzelm parents: 48791 diff changeset	46	session.thy_load.asInstanceOf[JEdit_Thy_Load]
44955 9adaf5cd4f1c tuned signature; wenzelm parents: 44954 diff changeset	47
48884 963b50ec6d73 clarified global get_recent_syntax: session always has its base_syntax, but it might be absent itself; wenzelm parents: 48872 diff changeset	48	def get_recent_syntax(): Option[Outer_Syntax] =
963b50ec6d73 clarified global get_recent_syntax: session always has its base_syntax, but it might be absent itself; wenzelm parents: 48872 diff changeset	49	{
963b50ec6d73 clarified global get_recent_syntax: session always has its base_syntax, but it might be absent itself; wenzelm parents: 48872 diff changeset	50	val current_session = session
49101 21c8d2070be9 continue with more robust dummy session after failed startup; wenzelm parents: 49100 diff changeset	51	if (current_session.recent_syntax == Outer_Syntax.empty) None
21c8d2070be9 continue with more robust dummy session after failed startup; wenzelm parents: 49100 diff changeset	52	else Some(current_session.recent_syntax)
48884 963b50ec6d73 clarified global get_recent_syntax: session always has its base_syntax, but it might be absent itself; wenzelm parents: 48872 diff changeset	53	}
963b50ec6d73 clarified global get_recent_syntax: session always has its base_syntax, but it might be absent itself; wenzelm parents: 48872 diff changeset	54
34784 02959dcea756 split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea); wenzelm parents: 34782 diff changeset	55
37164 8b4617ad1593 reuse main view.font from jEdit; wenzelm parents: 37068 diff changeset	56	/* font */
8b4617ad1593 reuse main view.font from jEdit; wenzelm parents: 37068 diff changeset	57
8b4617ad1593 reuse main view.font from jEdit; wenzelm parents: 37068 diff changeset	58	def font_family(): String = jEdit.getProperty("view.font")
8b4617ad1593 reuse main view.font from jEdit; wenzelm parents: 37068 diff changeset	59
37019 8f747cee4e27 zoom font size; wenzelm parents: 36814 diff changeset	60	def font_size(): Float =
8f747cee4e27 zoom font size; wenzelm parents: 36814 diff changeset	61	(jEdit.getIntegerProperty("view.fontsize", 16) *
49245 cb70157293c0 manage Isabelle/jEdit options as Isabelle/Scala options (with persistent preferences); wenzelm parents: 49195 diff changeset	62	options.int("jedit_relative_font_size")).toFloat / 100
36814 dc85664dbf6d support Isabelle plugin properties with defaults; wenzelm parents: 36760 diff changeset	63
34618 e45052ff7233 added Boolean_Property, Int_Property; wenzelm parents: 34615 diff changeset	64
37201 8517a650cfdc control tooltip font via Swing HTML, with tooltip-font-size property; wenzelm parents: 37177 diff changeset	65	/* tooltip markup */
8517a650cfdc control tooltip font via Swing HTML, with tooltip-font-size property; wenzelm parents: 37177 diff changeset	66
8517a650cfdc control tooltip font via Swing HTML, with tooltip-font-size property; wenzelm parents: 37177 diff changeset	67	def tooltip(text: String): String =
37203 c4261f3bbdd7 more flexibile font size via CSS <style> instead of old <font> element; wenzelm parents: 37201 diff changeset	68	"<html><pre style=\"font-family: " + font_family() + "; font-size: " +
49245 cb70157293c0 manage Isabelle/jEdit options as Isabelle/Scala options (with persistent preferences); wenzelm parents: 49195 diff changeset	69	options.int("jedit_tooltip_font_size").toString + "px; \">" + // FIXME proper scaling (!?)
37203 c4261f3bbdd7 more flexibile font size via CSS <style> instead of old <font> element; wenzelm parents: 37201 diff changeset	70	HTML.encode(text) + "</pre></html>"
37201 8517a650cfdc control tooltip font via Swing HTML, with tooltip-font-size property; wenzelm parents: 37177 diff changeset	71
44699 5199ee17c7d7 property "tooltip-dismiss-delay" is edited in ms, not seconds; wenzelm parents: 44615 diff changeset	72	private val tooltip_lb = Time.seconds(0.5)
5199ee17c7d7 property "tooltip-dismiss-delay" is edited in ms, not seconds; wenzelm parents: 44615 diff changeset	73	private val tooltip_ub = Time.seconds(60.0)
40849 09270033330e store tooltip-dismiss-delay as Double(seconds); wenzelm parents: 40848 diff changeset	74	def tooltip_dismiss_delay(): Time =
49245 cb70157293c0 manage Isabelle/jEdit options as Isabelle/Scala options (with persistent preferences); wenzelm parents: 49195 diff changeset	75	Time.seconds(options.real("jedit_tooltip_dismiss_delay")) max tooltip_lb min tooltip_ub
38854 eb6a35be18ca Isabelle/jEdit property for global tooltip dismiss delay; wenzelm parents: 38843 diff changeset	76
eb6a35be18ca Isabelle/jEdit property for global tooltip dismiss delay; wenzelm parents: 38843 diff changeset	77	def setup_tooltips()
eb6a35be18ca Isabelle/jEdit property for global tooltip dismiss delay; wenzelm parents: 38843 diff changeset	78	{
eb6a35be18ca Isabelle/jEdit property for global tooltip dismiss delay; wenzelm parents: 38843 diff changeset	79	Swing_Thread.now {
eb6a35be18ca Isabelle/jEdit property for global tooltip dismiss delay; wenzelm parents: 38843 diff changeset	80	val manager = javax.swing.ToolTipManager.sharedInstance
40849 09270033330e store tooltip-dismiss-delay as Double(seconds); wenzelm parents: 40848 diff changeset	81	manager.setDismissDelay(tooltip_dismiss_delay().ms.toInt)
38854 eb6a35be18ca Isabelle/jEdit property for global tooltip dismiss delay; wenzelm parents: 38843 diff changeset	82	}
eb6a35be18ca Isabelle/jEdit property for global tooltip dismiss delay; wenzelm parents: 38843 diff changeset	83	}
eb6a35be18ca Isabelle/jEdit property for global tooltip dismiss delay; wenzelm parents: 38843 diff changeset	84
37201 8517a650cfdc control tooltip font via Swing HTML, with tooltip-font-size property; wenzelm parents: 37177 diff changeset	85
39241 e9a442606db3 Isabelle.load_icon with some sanity checks; wenzelm parents: 39167 diff changeset	86	/* icons */
e9a442606db3 Isabelle.load_icon with some sanity checks; wenzelm parents: 39167 diff changeset	87
e9a442606db3 Isabelle.load_icon with some sanity checks; wenzelm parents: 39167 diff changeset	88	def load_icon(name: String): javax.swing.Icon =
e9a442606db3 Isabelle.load_icon with some sanity checks; wenzelm parents: 39167 diff changeset	89	{
e9a442606db3 Isabelle.load_icon with some sanity checks; wenzelm parents: 39167 diff changeset	90	val icon = GUIUtilities.loadIcon(name)
e9a442606db3 Isabelle.load_icon with some sanity checks; wenzelm parents: 39167 diff changeset	91	if (icon.getIconWidth < 0 \|\| icon.getIconHeight < 0)
39630 44181423183a explicit Session.Phase indication with associated event bus; wenzelm parents: 39628 diff changeset	92	Log.log(Log.ERROR, icon, "Bad icon: " + name)
39241 e9a442606db3 Isabelle.load_icon with some sanity checks; wenzelm parents: 39167 diff changeset	93	icon
e9a442606db3 Isabelle.load_icon with some sanity checks; wenzelm parents: 39167 diff changeset	94	}
e9a442606db3 Isabelle.load_icon with some sanity checks; wenzelm parents: 39167 diff changeset	95
e9a442606db3 Isabelle.load_icon with some sanity checks; wenzelm parents: 39167 diff changeset	96
44580 3bc9a215a56d some support for hyperlinks between different buffers; wenzelm parents: 44577 diff changeset	97	/* buffers */
3bc9a215a56d some support for hyperlinks between different buffers; wenzelm parents: 44577 diff changeset	98
3bc9a215a56d some support for hyperlinks between different buffers; wenzelm parents: 44577 diff changeset	99	def swing_buffer_lock[A](buffer: JEditBuffer)(body: => A): A =
3bc9a215a56d some support for hyperlinks between different buffers; wenzelm parents: 44577 diff changeset	100	Swing_Thread.now { buffer_lock(buffer) { body } }
3bc9a215a56d some support for hyperlinks between different buffers; wenzelm parents: 44577 diff changeset	101
3bc9a215a56d some support for hyperlinks between different buffers; wenzelm parents: 44577 diff changeset	102	def buffer_text(buffer: JEditBuffer): String =
3bc9a215a56d some support for hyperlinks between different buffers; wenzelm parents: 44577 diff changeset	103	buffer_lock(buffer) { buffer.getText(0, buffer.getLength) }
3bc9a215a56d some support for hyperlinks between different buffers; wenzelm parents: 44577 diff changeset	104
3bc9a215a56d some support for hyperlinks between different buffers; wenzelm parents: 44577 diff changeset	105	def buffer_name(buffer: Buffer): String = buffer.getSymlinkPath
3bc9a215a56d some support for hyperlinks between different buffers; wenzelm parents: 44577 diff changeset	106
48718 73e6c22e2d94 more structural parsing for minor modes; wenzelm parents: 48717 diff changeset	107	def buffer_node_dummy(buffer: Buffer): Option[Document.Node.Name] =
73e6c22e2d94 more structural parsing for minor modes; wenzelm parents: 48717 diff changeset	108	Some(Document.Node.Name(buffer_name(buffer), buffer.getDirectory, buffer.getName))
73e6c22e2d94 more structural parsing for minor modes; wenzelm parents: 48717 diff changeset	109
73e6c22e2d94 more structural parsing for minor modes; wenzelm parents: 48717 diff changeset	110	def buffer_node_name(buffer: Buffer): Option[Document.Node.Name] =
73e6c22e2d94 more structural parsing for minor modes; wenzelm parents: 48717 diff changeset	111	{
73e6c22e2d94 more structural parsing for minor modes; wenzelm parents: 48717 diff changeset	112	val name = buffer_name(buffer)
73e6c22e2d94 more structural parsing for minor modes; wenzelm parents: 48717 diff changeset	113	Thy_Header.thy_name(name).map(theory => Document.Node.Name(name, buffer.getDirectory, theory))
73e6c22e2d94 more structural parsing for minor modes; wenzelm parents: 48717 diff changeset	114	}
73e6c22e2d94 more structural parsing for minor modes; wenzelm parents: 48717 diff changeset	115
44580 3bc9a215a56d some support for hyperlinks between different buffers; wenzelm parents: 44577 diff changeset	116
38221 e0f00f0945b4 misc tuning and clarification; wenzelm parents: 37557 diff changeset	117	/* 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	118
37177 17331ca75044 avoid deprecated Iterator.fromArray; wenzelm parents: 37164 diff changeset	119	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	120
44580 3bc9a215a56d some support for hyperlinks between different buffers; wenzelm parents: 44577 diff changeset	121	def jedit_buffer(name: String): Option[Buffer] =
3bc9a215a56d some support for hyperlinks between different buffers; wenzelm parents: 44577 diff changeset	122	jedit_buffers().find(buffer => buffer_name(buffer) == name)
3bc9a215a56d some support for hyperlinks between different buffers; wenzelm parents: 44577 diff changeset	123
37177 17331ca75044 avoid deprecated Iterator.fromArray; wenzelm parents: 37164 diff changeset	124	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	125
02959dcea756 split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea); wenzelm parents: 34782 diff changeset	126	def jedit_text_areas(view: View): Iterator[JEditTextArea] =
37177 17331ca75044 avoid deprecated Iterator.fromArray; wenzelm parents: 37164 diff changeset	127	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	128
02959dcea756 split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea); wenzelm parents: 34782 diff changeset	129	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	130	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	131
02959dcea756 split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea); wenzelm parents: 34782 diff changeset	132	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	133	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	134
38843 d95522496593 more careful locking of jEdit buffer; wenzelm parents: 38640 diff changeset	135	def buffer_lock[A](buffer: JEditBuffer)(body: => A): A =
38640 105d1f112da5 sporadic locking of jEdit buffer; wenzelm parents: 38222 diff changeset	136	{
105d1f112da5 sporadic locking of jEdit buffer; wenzelm parents: 38222 diff changeset	137	try { buffer.readLock(); body }
105d1f112da5 sporadic locking of jEdit buffer; wenzelm parents: 38222 diff changeset	138	finally { buffer.readUnlock() }
105d1f112da5 sporadic locking of jEdit buffer; wenzelm parents: 38222 diff changeset	139	}
105d1f112da5 sporadic locking of jEdit buffer; wenzelm parents: 38222 diff changeset	140
34784 02959dcea756 split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea); wenzelm parents: 34782 diff changeset	141
43449 591598bc52bc convenience functions; wenzelm parents: 43443 diff changeset	142	/* document model and view */
591598bc52bc convenience functions; wenzelm parents: 43443 diff changeset	143
591598bc52bc convenience functions; wenzelm parents: 43443 diff changeset	144	def document_model(buffer: Buffer): Option[Document_Model] = Document_Model(buffer)
591598bc52bc convenience functions; wenzelm parents: 43443 diff changeset	145	def document_view(text_area: JEditTextArea): Option[Document_View] = Document_View(text_area)
591598bc52bc convenience functions; wenzelm parents: 43443 diff changeset	146
44379 1079ab6b342b added official Text.Range.Ordering; wenzelm parents: 44238 diff changeset	147	def document_views(buffer: Buffer): List[Document_View] =
1079ab6b342b added official Text.Range.Ordering; wenzelm parents: 44238 diff changeset	148	for {
1079ab6b342b added official Text.Range.Ordering; wenzelm parents: 44238 diff changeset	149	text_area <- jedit_text_areas(buffer).toList
46997 395b7277ed76 misc tuning to accomodate scala-2.10.0-M2; wenzelm parents: 46918 diff changeset	150	doc_view = document_view(text_area)
44379 1079ab6b342b added official Text.Range.Ordering; wenzelm parents: 44238 diff changeset	151	if doc_view.isDefined
1079ab6b342b added official Text.Range.Ordering; wenzelm parents: 44238 diff changeset	152	} yield doc_view.get
1079ab6b342b added official Text.Range.Ordering; wenzelm parents: 44238 diff changeset	153
47058 34761733526c refined init_model: allow change of buffer name as caused by "Save as", for example; wenzelm parents: 46997 diff changeset	154	def exit_model(buffer: Buffer)
34761733526c refined init_model: allow change of buffer name as caused by "Save as", for example; wenzelm parents: 46997 diff changeset	155	{
34761733526c refined init_model: allow change of buffer name as caused by "Save as", for example; wenzelm parents: 46997 diff changeset	156	swing_buffer_lock(buffer) {
34761733526c refined init_model: allow change of buffer name as caused by "Save as", for example; wenzelm parents: 46997 diff changeset	157	jedit_text_areas(buffer).foreach(Document_View.exit)
34761733526c refined init_model: allow change of buffer name as caused by "Save as", for example; wenzelm parents: 46997 diff changeset	158	Document_Model.exit(buffer)
34761733526c refined init_model: allow change of buffer name as caused by "Save as", for example; wenzelm parents: 46997 diff changeset	159	}
34761733526c refined init_model: allow change of buffer name as caused by "Save as", for example; wenzelm parents: 46997 diff changeset	160	}
34761733526c refined init_model: allow change of buffer name as caused by "Save as", for example; wenzelm parents: 46997 diff changeset	161
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	162	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	163	{
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	164	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	165	val opt_model =
48717 622251b2b0f1 clarified Sidekick configuration, including minor modes; wenzelm parents: 48709 diff changeset	166	buffer_node_name(buffer) match {
622251b2b0f1 clarified Sidekick configuration, including minor modes; wenzelm parents: 48709 diff changeset	167	case Some(node_name) =>
47058 34761733526c refined init_model: allow change of buffer name as caused by "Save as", for example; wenzelm parents: 46997 diff changeset	168	document_model(buffer) match {
34761733526c refined init_model: allow change of buffer name as caused by "Save as", for example; wenzelm parents: 46997 diff changeset	169	case Some(model) if model.name == node_name => Some(model)
34761733526c refined init_model: allow change of buffer name as caused by "Save as", for example; wenzelm parents: 46997 diff changeset	170	case _ => Some(Document_Model.init(session, buffer, node_name))
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	171	}
47058 34761733526c refined init_model: allow change of buffer name as caused by "Save as", for example; wenzelm parents: 46997 diff changeset	172	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	173	}
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	174	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	175	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	176	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	177	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	178	}
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	179	}
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	180	}
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	181	}
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	182
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	183	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	184	{
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	185	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	186	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	187	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	188	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	189	}
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	190	}
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	191	}
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	192
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	193	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	194	{
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	195	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	196	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	197	}
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	198	}
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	199
43449 591598bc52bc convenience functions; wenzelm parents: 43443 diff changeset	200
37068 07936a4efe93 access statically typed dockable windows; wenzelm parents: 37019 diff changeset	201	/* dockable windows */
07936a4efe93 access statically typed dockable windows; wenzelm parents: 37019 diff changeset	202
07936a4efe93 access statically typed dockable windows; wenzelm parents: 37019 diff changeset	203	private def wm(view: View): DockableWindowManager = view.getDockableWindowManager
07936a4efe93 access statically typed dockable windows; wenzelm parents: 37019 diff changeset	204
39515 57ceabb0bb8e basic setup for prover session panel; wenzelm parents: 39241 diff changeset	205	def docked_session(view: View): Option[Session_Dockable] =
57ceabb0bb8e basic setup for prover session panel; wenzelm parents: 39241 diff changeset	206	wm(view).getDockableWindow("isabelle-session") match {
57ceabb0bb8e basic setup for prover session panel; wenzelm parents: 39241 diff changeset	207	case dockable: Session_Dockable => Some(dockable)
57ceabb0bb8e basic setup for prover session panel; wenzelm parents: 39241 diff changeset	208	case _ => None
57ceabb0bb8e basic setup for prover session panel; wenzelm parents: 39241 diff changeset	209	}
57ceabb0bb8e basic setup for prover session panel; wenzelm parents: 39241 diff changeset	210
37068 07936a4efe93 access statically typed dockable windows; wenzelm parents: 37019 diff changeset	211	def docked_output(view: View): Option[Output_Dockable] =
07936a4efe93 access statically typed dockable windows; wenzelm parents: 37019 diff changeset	212	wm(view).getDockableWindow("isabelle-output") match {
07936a4efe93 access statically typed dockable windows; wenzelm parents: 37019 diff changeset	213	case dockable: Output_Dockable => Some(dockable)
07936a4efe93 access statically typed dockable windows; wenzelm parents: 37019 diff changeset	214	case _ => None
07936a4efe93 access statically typed dockable windows; wenzelm parents: 37019 diff changeset	215	}
07936a4efe93 access statically typed dockable windows; wenzelm parents: 37019 diff changeset	216
07936a4efe93 access statically typed dockable windows; wenzelm parents: 37019 diff changeset	217	def docked_raw_output(view: View): Option[Raw_Output_Dockable] =
07936a4efe93 access statically typed dockable windows; wenzelm parents: 37019 diff changeset	218	wm(view).getDockableWindow("isabelle-raw-output") match {
07936a4efe93 access statically typed dockable windows; wenzelm parents: 37019 diff changeset	219	case dockable: Raw_Output_Dockable => Some(dockable)
07936a4efe93 access statically typed dockable windows; wenzelm parents: 37019 diff changeset	220	case _ => None
07936a4efe93 access statically typed dockable windows; wenzelm parents: 37019 diff changeset	221	}
07936a4efe93 access statically typed dockable windows; wenzelm parents: 37019 diff changeset	222
07936a4efe93 access statically typed dockable windows; wenzelm parents: 37019 diff changeset	223	def docked_protocol(view: View): Option[Protocol_Dockable] =
07936a4efe93 access statically typed dockable windows; wenzelm parents: 37019 diff changeset	224	wm(view).getDockableWindow("isabelle-protocol") match {
07936a4efe93 access statically typed dockable windows; wenzelm parents: 37019 diff changeset	225	case dockable: Protocol_Dockable => Some(dockable)
07936a4efe93 access statically typed dockable windows; wenzelm parents: 37019 diff changeset	226	case _ => None
07936a4efe93 access statically typed dockable windows; wenzelm parents: 37019 diff changeset	227	}
07936a4efe93 access statically typed dockable windows; wenzelm parents: 37019 diff changeset	228
07936a4efe93 access statically typed dockable windows; wenzelm parents: 37019 diff changeset	229
39517 e036c67448e6 separate Isabelle.logic_selector; wenzelm parents: 39515 diff changeset	230	/* logic image */
e036c67448e6 separate Isabelle.logic_selector; wenzelm parents: 39515 diff changeset	231
e036c67448e6 separate Isabelle.logic_selector; wenzelm parents: 39515 diff changeset	232	def default_logic(): String =
e036c67448e6 separate Isabelle.logic_selector; wenzelm parents: 39515 diff changeset	233	{
43661 39fdbd814c7f quasi-static Isabelle_System -- reduced tendency towards "functorial style"; wenzelm parents: 43648 diff changeset	234	val logic = Isabelle_System.getenv("JEDIT_LOGIC")
39517 e036c67448e6 separate Isabelle.logic_selector; wenzelm parents: 39515 diff changeset	235	if (logic != "") logic
43661 39fdbd814c7f quasi-static Isabelle_System -- reduced tendency towards "functorial style"; wenzelm parents: 43648 diff changeset	236	else Isabelle_System.getenv_strict("ISABELLE_LOGIC")
39517 e036c67448e6 separate Isabelle.logic_selector; wenzelm parents: 39515 diff changeset	237	}
e036c67448e6 separate Isabelle.logic_selector; wenzelm parents: 39515 diff changeset	238
e036c67448e6 separate Isabelle.logic_selector; wenzelm parents: 39515 diff changeset	239	class Logic_Entry(val name: String, val description: String)
e036c67448e6 separate Isabelle.logic_selector; wenzelm parents: 39515 diff changeset	240	{
e036c67448e6 separate Isabelle.logic_selector; wenzelm parents: 39515 diff changeset	241	override def toString = description
e036c67448e6 separate Isabelle.logic_selector; wenzelm parents: 39515 diff changeset	242	}
e036c67448e6 separate Isabelle.logic_selector; wenzelm parents: 39515 diff changeset	243
e036c67448e6 separate Isabelle.logic_selector; wenzelm parents: 39515 diff changeset	244	def logic_selector(logic: String): ComboBox[Logic_Entry] =
e036c67448e6 separate Isabelle.logic_selector; wenzelm parents: 39515 diff changeset	245	{
e036c67448e6 separate Isabelle.logic_selector; wenzelm parents: 39515 diff changeset	246	val entries =
e036c67448e6 separate Isabelle.logic_selector; wenzelm parents: 39515 diff changeset	247	new Logic_Entry("", "default (" + default_logic() + ")") ::
43661 39fdbd814c7f quasi-static Isabelle_System -- reduced tendency towards "functorial style"; wenzelm parents: 43648 diff changeset	248	Isabelle_System.find_logics().map(name => new Logic_Entry(name, name))
39517 e036c67448e6 separate Isabelle.logic_selector; wenzelm parents: 39515 diff changeset	249	val component = new ComboBox(entries)
e036c67448e6 separate Isabelle.logic_selector; wenzelm parents: 39515 diff changeset	250	entries.find(_.name == logic) match {
e036c67448e6 separate Isabelle.logic_selector; wenzelm parents: 39515 diff changeset	251	case None =>
e036c67448e6 separate Isabelle.logic_selector; wenzelm parents: 39515 diff changeset	252	case Some(entry) => component.selection.item = entry
e036c67448e6 separate Isabelle.logic_selector; wenzelm parents: 39515 diff changeset	253	}
39702 d7c256cb2797 Session_Dockable: more startup controls; wenzelm parents: 39701 diff changeset	254	component.tooltip = "Isabelle logic image"
39517 e036c67448e6 separate Isabelle.logic_selector; wenzelm parents: 39515 diff changeset	255	component
e036c67448e6 separate Isabelle.logic_selector; wenzelm parents: 39515 diff changeset	256	}
39702 d7c256cb2797 Session_Dockable: more startup controls; wenzelm parents: 39701 diff changeset	257
48870 4accee106f0f clarified initialization of Thy_Load, Thy_Info, Session; wenzelm parents: 48791 diff changeset	258	def session_args(): List[String] =
39702 d7c256cb2797 Session_Dockable: more startup controls; wenzelm parents: 39701 diff changeset	259	{
43670 7f933761764b prefer space_explode/split_lines as in Isabelle/ML; wenzelm parents: 43661 diff changeset	260	val modes = space_explode(',', Isabelle_System.getenv("JEDIT_PRINT_MODE")).map("-m" + _)
49245 cb70157293c0 manage Isabelle/jEdit options as Isabelle/Scala options (with persistent preferences); wenzelm parents: 49195 diff changeset	261	val logic =
cb70157293c0 manage Isabelle/jEdit options as Isabelle/Scala options (with persistent preferences); wenzelm parents: 49195 diff changeset	262	Isabelle.options.string("jedit_logic") match {
cb70157293c0 manage Isabelle/jEdit options as Isabelle/Scala options (with persistent preferences); wenzelm parents: 49195 diff changeset	263	case "" => Isabelle.default_logic()
cb70157293c0 manage Isabelle/jEdit options as Isabelle/Scala options (with persistent preferences); wenzelm parents: 49195 diff changeset	264	case logic => logic
cb70157293c0 manage Isabelle/jEdit options as Isabelle/Scala options (with persistent preferences); wenzelm parents: 49195 diff changeset	265	}
48870 4accee106f0f clarified initialization of Thy_Load, Thy_Info, Session; wenzelm parents: 48791 diff changeset	266	modes ::: List(logic)
4accee106f0f clarified initialization of Thy_Load, Thy_Info, Session; wenzelm parents: 48791 diff changeset	267	}
4accee106f0f clarified initialization of Thy_Load, Thy_Info, Session; wenzelm parents: 48791 diff changeset	268
49098 673e0ed547af bypass slow check for inlined files, where it is not really required; wenzelm parents: 48884 diff changeset	269	def session_content(inlined_files: Boolean): Build.Session_Content =
48870 4accee106f0f clarified initialization of Thy_Load, Thy_Info, Session; wenzelm parents: 48791 diff changeset	270	{
4accee106f0f clarified initialization of Thy_Load, Thy_Info, Session; wenzelm parents: 48791 diff changeset	271	val dirs = Path.split(Isabelle_System.getenv("JEDIT_SESSION_DIRS"))
4accee106f0f clarified initialization of Thy_Load, Thy_Info, Session; wenzelm parents: 48791 diff changeset	272	val name = Path.explode(session_args().last).base.implode // FIXME more robust
49098 673e0ed547af bypass slow check for inlined files, where it is not really required; wenzelm parents: 48884 diff changeset	273	Build.session_content(inlined_files, dirs, name).check_errors
39702 d7c256cb2797 Session_Dockable: more startup controls; wenzelm parents: 39701 diff changeset	274	}
44238 36120feb70ed some convenience actions/shortcuts for control symbols; wenzelm parents: 44225 diff changeset	275
36120feb70ed some convenience actions/shortcuts for control symbols; wenzelm parents: 44225 diff changeset	276
36120feb70ed some convenience actions/shortcuts for control symbols; wenzelm parents: 44225 diff changeset	277	/* convenience actions */
36120feb70ed some convenience actions/shortcuts for control symbols; wenzelm parents: 44225 diff changeset	278
36120feb70ed some convenience actions/shortcuts for control symbols; wenzelm parents: 44225 diff changeset	279	private def user_input(text_area: JEditTextArea, s1: String, s2: String = "")
36120feb70ed some convenience actions/shortcuts for control symbols; wenzelm parents: 44225 diff changeset	280	{
36120feb70ed some convenience actions/shortcuts for control symbols; wenzelm parents: 44225 diff changeset	281	s1.foreach(text_area.userInput(_))
36120feb70ed some convenience actions/shortcuts for control symbols; wenzelm parents: 44225 diff changeset	282	s2.foreach(text_area.userInput(_))
36120feb70ed some convenience actions/shortcuts for control symbols; wenzelm parents: 44225 diff changeset	283	s2.foreach(_ => text_area.goToPrevCharacter(false))
36120feb70ed some convenience actions/shortcuts for control symbols; wenzelm parents: 44225 diff changeset	284	}
36120feb70ed some convenience actions/shortcuts for control symbols; wenzelm parents: 44225 diff changeset	285
36120feb70ed some convenience actions/shortcuts for control symbols; wenzelm parents: 44225 diff changeset	286	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	287	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	288	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	289	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	290	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	291	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	292	def input_bold(text_area: JEditTextArea): Unit = user_input(text_area, Symbol.bold_decoded)
44864 e50557cb0eb6 explicit jEdit actions -- to enable key mappings, for example; wenzelm parents: 44721 diff changeset	293
e50557cb0eb6 explicit jEdit actions -- to enable key mappings, for example; wenzelm parents: 44721 diff changeset	294	def check_buffer(buffer: Buffer)
e50557cb0eb6 explicit jEdit actions -- to enable key mappings, for example; wenzelm parents: 44721 diff changeset	295	{
e50557cb0eb6 explicit jEdit actions -- to enable key mappings, for example; wenzelm parents: 44721 diff changeset	296	document_model(buffer) match {
e50557cb0eb6 explicit jEdit actions -- to enable key mappings, for example; wenzelm parents: 44721 diff changeset	297	case None =>
e50557cb0eb6 explicit jEdit actions -- to enable key mappings, for example; wenzelm parents: 44721 diff changeset	298	case Some(model) => model.full_perspective()
e50557cb0eb6 explicit jEdit actions -- to enable key mappings, for example; wenzelm parents: 44721 diff changeset	299	}
e50557cb0eb6 explicit jEdit actions -- to enable key mappings, for example; wenzelm parents: 44721 diff changeset	300	}
e50557cb0eb6 explicit jEdit actions -- to enable key mappings, for example; wenzelm parents: 44721 diff changeset	301
e50557cb0eb6 explicit jEdit actions -- to enable key mappings, for example; wenzelm parents: 44721 diff changeset	302	def cancel_execution() { session.cancel_execution() }
34318 c13e168a8ae6 original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout; wenzelm parents: diff changeset	303	}
c13e168a8ae6 original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout; wenzelm parents: diff changeset	304
34429 03afc73e185f tuned; wenzelm parents: 34422 diff changeset	305
34618 e45052ff7233 added Boolean_Property, Int_Property; wenzelm parents: 34615 diff changeset	306	class Plugin extends EBPlugin
e45052ff7233 added Boolean_Property, Int_Property; wenzelm parents: 34615 diff changeset	307	{
44577 96b6388d06c4 separate module for jEdit primitives for loading theory files; wenzelm parents: 44574 diff changeset	308	/* theory files */
44574 24444588fddd actual auto loading of required files; wenzelm parents: 44573 diff changeset	309
44573 51f8895b9ad9 some dialog for auto loading of required files (still inactive); wenzelm parents: 44434 diff changeset	310	private lazy val delay_load =
44574 24444588fddd actual auto loading of required files; wenzelm parents: 44573 diff changeset	311	Swing_Thread.delay_last(Isabelle.session.load_delay)
24444588fddd actual auto loading of required files; wenzelm parents: 44573 diff changeset	312	{
44963 4662dddc2fd8 explicit check_file wrt. jEdit VFS, to avoid slightly confusing empty buffer after IO error; wenzelm parents: 44955 diff changeset	313	val view = jEdit.getActiveView()
4662dddc2fd8 explicit check_file wrt. jEdit VFS, to avoid slightly confusing empty buffer after IO error; wenzelm parents: 44955 diff changeset	314
44574 24444588fddd actual auto loading of required files; wenzelm parents: 44573 diff changeset	315	val buffers = Isabelle.jedit_buffers().toList
46761 b0a797158e34 avoid buffer loading overrun; wenzelm parents: 46740 diff changeset	316	if (buffers.forall(_.isLoaded)) {
b0a797158e34 avoid buffer loading overrun; wenzelm parents: 46740 diff changeset	317	def loaded_buffer(name: String): Boolean =
b0a797158e34 avoid buffer loading overrun; wenzelm parents: 46740 diff changeset	318	buffers.exists(buffer => Isabelle.buffer_name(buffer) == name)
44574 24444588fddd actual auto loading of required files; wenzelm parents: 44573 diff changeset	319
46761 b0a797158e34 avoid buffer loading overrun; wenzelm parents: 46740 diff changeset	320	val thys =
b0a797158e34 avoid buffer loading overrun; wenzelm parents: 46740 diff changeset	321	for (buffer <- buffers; model <- Isabelle.document_model(buffer))
b0a797158e34 avoid buffer loading overrun; wenzelm parents: 46740 diff changeset	322	yield model.name
b0a797158e34 avoid buffer loading overrun; wenzelm parents: 46740 diff changeset	323
48870 4accee106f0f clarified initialization of Thy_Load, Thy_Info, Session; wenzelm parents: 48791 diff changeset	324	val thy_info = new Thy_Info(Isabelle.thy_load)
46761 b0a797158e34 avoid buffer loading overrun; wenzelm parents: 46740 diff changeset	325	// FIXME avoid I/O in Swing thread!?!
49098 673e0ed547af bypass slow check for inlined files, where it is not really required; wenzelm parents: 48884 diff changeset	326	val files = thy_info.dependencies(true, thys).deps.map(_._1.node).
46761 b0a797158e34 avoid buffer loading overrun; wenzelm parents: 46740 diff changeset	327	filter(file => !loaded_buffer(file) && Isabelle.thy_load.check_file(view, file))
44574 24444588fddd actual auto loading of required files; wenzelm parents: 44573 diff changeset	328
46761 b0a797158e34 avoid buffer loading overrun; wenzelm parents: 46740 diff changeset	329	if (!files.isEmpty) {
b0a797158e34 avoid buffer loading overrun; wenzelm parents: 46740 diff changeset	330	val files_list = new ListView(files.sorted)
b0a797158e34 avoid buffer loading overrun; wenzelm parents: 46740 diff changeset	331	for (i <- 0 until files.length)
b0a797158e34 avoid buffer loading overrun; wenzelm parents: 46740 diff changeset	332	files_list.selection.indices += i
44606 b625650aa2db improved auto loading: selectable file list; wenzelm parents: 44580 diff changeset	333
46761 b0a797158e34 avoid buffer loading overrun; wenzelm parents: 46740 diff changeset	334	val answer =
b0a797158e34 avoid buffer loading overrun; wenzelm parents: 46740 diff changeset	335	Library.confirm_dialog(view,
b0a797158e34 avoid buffer loading overrun; wenzelm parents: 46740 diff changeset	336	"Auto loading of required files",
b0a797158e34 avoid buffer loading overrun; wenzelm parents: 46740 diff changeset	337	JOptionPane.YES_NO_OPTION,
b0a797158e34 avoid buffer loading overrun; wenzelm parents: 46740 diff changeset	338	"The following files are required to resolve theory imports.",
b0a797158e34 avoid buffer loading overrun; wenzelm parents: 46740 diff changeset	339	"Reload selected files now?",
b0a797158e34 avoid buffer loading overrun; wenzelm parents: 46740 diff changeset	340	new ScrollPane(files_list))
b0a797158e34 avoid buffer loading overrun; wenzelm parents: 46740 diff changeset	341	if (answer == 0) {
b0a797158e34 avoid buffer loading overrun; wenzelm parents: 46740 diff changeset	342	files.foreach(file =>
b0a797158e34 avoid buffer loading overrun; wenzelm parents: 46740 diff changeset	343	if (files_list.selection.items.contains(file))
b0a797158e34 avoid buffer loading overrun; wenzelm parents: 46740 diff changeset	344	jEdit.openFile(null: View, file))
b0a797158e34 avoid buffer loading overrun; wenzelm parents: 46740 diff changeset	345	}
b0a797158e34 avoid buffer loading overrun; wenzelm parents: 46740 diff changeset	346	}
44606 b625650aa2db improved auto loading: selectable file list; wenzelm parents: 44580 diff changeset	347	}
44574 24444588fddd actual auto loading of required files; wenzelm parents: 44573 diff changeset	348	}
44573 51f8895b9ad9 some dialog for auto loading of required files (still inactive); wenzelm parents: 44434 diff changeset	349
44574 24444588fddd actual auto loading of required files; wenzelm parents: 44573 diff changeset	350
24444588fddd actual auto loading of required files; wenzelm parents: 44573 diff changeset	351	/* session manager */
44573 51f8895b9ad9 some dialog for auto loading of required files (still inactive); wenzelm parents: 44434 diff changeset	352
39633 26a28110ece5 simplified Session.Phase; wenzelm parents: 39631 diff changeset	353	private val session_manager = actor {
26a28110ece5 simplified Session.Phase; wenzelm parents: 39631 diff changeset	354	loop {
26a28110ece5 simplified Session.Phase; wenzelm parents: 39631 diff changeset	355	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	356	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	357	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	358	case Session.Failed =>
46918 1752164d916b prefer asynchronous context switch from actor to swing thread, to reduce danger of deadlocks; wenzelm parents: 46771 diff changeset	359	Swing_Thread.later {
48022 e237a3fc7ba3 tuned message; wenzelm parents: 48020 diff changeset	360	Library.error_dialog(jEdit.getActiveView, "Prover process failure",
e237a3fc7ba3 tuned message; wenzelm parents: 48020 diff changeset	361	"Isabelle Syslog", Library.scrollable_text(Isabelle.session.current_syslog()))
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	362	}
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	363
44573 51f8895b9ad9 some dialog for auto loading of required files (still inactive); wenzelm parents: 44434 diff changeset	364	case Session.Ready =>
51f8895b9ad9 some dialog for auto loading of required files (still inactive); wenzelm parents: 44434 diff changeset	365	Isabelle.jedit_buffers.foreach(Isabelle.init_model)
49195 9d10bd85c1be more explicit Delay operations; wenzelm parents: 49101 diff changeset	366	Swing_Thread.later { delay_load.invoke() }
44573 51f8895b9ad9 some dialog for auto loading of required files (still inactive); wenzelm parents: 44434 diff changeset	367
46740 852baa599351 explicitly revoke delay, to avoid spurious timer events after deactivation of related components; wenzelm parents: 46204 diff changeset	368	case Session.Shutdown =>
852baa599351 explicitly revoke delay, to avoid spurious timer events after deactivation of related components; wenzelm parents: 46204 diff changeset	369	Isabelle.jedit_buffers.foreach(Isabelle.exit_model)
49195 9d10bd85c1be more explicit Delay operations; wenzelm parents: 49101 diff changeset	370	Swing_Thread.later { delay_load.revoke() }
46740 852baa599351 explicitly revoke delay, to avoid spurious timer events after deactivation of related components; wenzelm parents: 46204 diff changeset	371
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	372	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	373	}
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	374	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	375	}
44181423183a explicit Session.Phase indication with associated event bus; wenzelm parents: 39628 diff changeset	376	}
44181423183a explicit Session.Phase indication with associated event bus; wenzelm parents: 39628 diff changeset	377	}
44181423183a explicit Session.Phase indication with associated event bus; wenzelm parents: 39628 diff changeset	378
44181423183a explicit Session.Phase indication with associated event bus; wenzelm parents: 39628 diff changeset	379
34618 e45052ff7233 added Boolean_Property, Int_Property; wenzelm parents: 34615 diff changeset	380	/* main plugin plumbing */
34433 3da749b53842 renamed Plugin.plugin to Plugin.self; wenzelm parents: 34429 diff changeset	381
34767 8dd19c5f8c56 added properties_changed event bus; wenzelm parents: 34764 diff changeset	382	override def handleMessage(message: EBMessage)
34618 e45052ff7233 added Boolean_Property, Int_Property; wenzelm parents: 34615 diff changeset	383	{
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	384	Swing_Thread.assert()
39630 44181423183a explicit Session.Phase indication with associated event bus; wenzelm parents: 39628 diff changeset	385
49099 10e899bb6530 more permissive handling of plugin startup failure; wenzelm parents: 49098 diff changeset	386	if (Isabelle.startup_failure.isDefined && !Isabelle.startup_notified) {
10e899bb6530 more permissive handling of plugin startup failure; wenzelm parents: 49098 diff changeset	387	message match {
49100 e7aecf2a5fc4 prefer old startup dialog scheme (cf. 514bb82514df); wenzelm parents: 49099 diff changeset	388	case msg: EditorStarted =>
e7aecf2a5fc4 prefer old startup dialog scheme (cf. 514bb82514df); wenzelm parents: 49099 diff changeset	389	Library.error_dialog(null, "Isabelle plugin startup failure",
49099 10e899bb6530 more permissive handling of plugin startup failure; wenzelm parents: 49098 diff changeset	390	Library.scrollable_text(Exn.message(Isabelle.startup_failure.get)),
10e899bb6530 more permissive handling of plugin startup failure; wenzelm parents: 49098 diff changeset	391	"Prover IDE inactive!")
10e899bb6530 more permissive handling of plugin startup failure; wenzelm parents: 49098 diff changeset	392	Isabelle.startup_notified = true
10e899bb6530 more permissive handling of plugin startup failure; wenzelm parents: 49098 diff changeset	393	case _ =>
10e899bb6530 more permissive handling of plugin startup failure; wenzelm parents: 49098 diff changeset	394	}
10e899bb6530 more permissive handling of plugin startup failure; wenzelm parents: 49098 diff changeset	395	}
10e899bb6530 more permissive handling of plugin startup failure; wenzelm parents: 49098 diff changeset	396
10e899bb6530 more permissive handling of plugin startup failure; wenzelm parents: 49098 diff changeset	397	if (Isabelle.startup_failure.isEmpty) {
10e899bb6530 more permissive handling of plugin startup failure; wenzelm parents: 49098 diff changeset	398	message match {
10e899bb6530 more permissive handling of plugin startup failure; wenzelm parents: 49098 diff changeset	399	case msg: EditorStarted =>
49245 cb70157293c0 manage Isabelle/jEdit options as Isabelle/Scala options (with persistent preferences); wenzelm parents: 49195 diff changeset	400	if (Isabelle.options.bool("jedit_auto_start"))
49099 10e899bb6530 more permissive handling of plugin startup failure; wenzelm parents: 49098 diff changeset	401	Isabelle.session.start(Isabelle.session_args())
37557 1ae272fd4082 refresh Isabelle token marker after buffer properties changed, e.g. when fold mode is switched; wenzelm parents: 37241 diff changeset	402
49099 10e899bb6530 more permissive handling of plugin startup failure; wenzelm parents: 49098 diff changeset	403	case msg: BufferUpdate
10e899bb6530 more permissive handling of plugin startup failure; wenzelm parents: 49098 diff changeset	404	if msg.getWhat == BufferUpdate.LOADED \|\| msg.getWhat == BufferUpdate.PROPERTIES_CHANGED =>
10e899bb6530 more permissive handling of plugin startup failure; wenzelm parents: 49098 diff changeset	405	if (Isabelle.session.is_ready) {
10e899bb6530 more permissive handling of plugin startup failure; wenzelm parents: 49098 diff changeset	406	val buffer = msg.getBuffer
10e899bb6530 more permissive handling of plugin startup failure; wenzelm parents: 49098 diff changeset	407	if (buffer != null && !buffer.isLoading) Isabelle.init_model(buffer)
49195 9d10bd85c1be more explicit Delay operations; wenzelm parents: 49101 diff changeset	408	Swing_Thread.later { delay_load.invoke() }
49099 10e899bb6530 more permissive handling of plugin startup failure; wenzelm parents: 49098 diff changeset	409	}
34784 02959dcea756 split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea); wenzelm parents: 34782 diff changeset	410
49099 10e899bb6530 more permissive handling of plugin startup failure; wenzelm parents: 49098 diff changeset	411	case msg: EditPaneUpdate
10e899bb6530 more permissive handling of plugin startup failure; wenzelm parents: 49098 diff changeset	412	if (msg.getWhat == EditPaneUpdate.BUFFER_CHANGING \|\|
10e899bb6530 more permissive handling of plugin startup failure; wenzelm parents: 49098 diff changeset	413	msg.getWhat == EditPaneUpdate.BUFFER_CHANGED \|\|
10e899bb6530 more permissive handling of plugin startup failure; wenzelm parents: 49098 diff changeset	414	msg.getWhat == EditPaneUpdate.CREATED \|\|
10e899bb6530 more permissive handling of plugin startup failure; wenzelm parents: 49098 diff changeset	415	msg.getWhat == EditPaneUpdate.DESTROYED) =>
10e899bb6530 more permissive handling of plugin startup failure; wenzelm parents: 49098 diff changeset	416	val edit_pane = msg.getEditPane
10e899bb6530 more permissive handling of plugin startup failure; wenzelm parents: 49098 diff changeset	417	val buffer = edit_pane.getBuffer
10e899bb6530 more permissive handling of plugin startup failure; wenzelm parents: 49098 diff changeset	418	val text_area = edit_pane.getTextArea
10e899bb6530 more permissive handling of plugin startup failure; wenzelm parents: 49098 diff changeset	419
10e899bb6530 more permissive handling of plugin startup failure; wenzelm parents: 49098 diff changeset	420	if (buffer != null && text_area != null) {
10e899bb6530 more permissive handling of plugin startup failure; wenzelm parents: 49098 diff changeset	421	if (msg.getWhat == EditPaneUpdate.BUFFER_CHANGED \|\|
10e899bb6530 more permissive handling of plugin startup failure; wenzelm parents: 49098 diff changeset	422	msg.getWhat == EditPaneUpdate.CREATED) {
10e899bb6530 more permissive handling of plugin startup failure; wenzelm parents: 49098 diff changeset	423	if (Isabelle.session.is_ready)
10e899bb6530 more permissive handling of plugin startup failure; wenzelm parents: 49098 diff changeset	424	Isabelle.init_view(buffer, text_area)
10e899bb6530 more permissive handling of plugin startup failure; wenzelm parents: 49098 diff changeset	425	}
10e899bb6530 more permissive handling of plugin startup failure; wenzelm parents: 49098 diff changeset	426	else Isabelle.exit_view(buffer, text_area)
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	427	}
34784 02959dcea756 split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea); wenzelm parents: 34782 diff changeset	428
49099 10e899bb6530 more permissive handling of plugin startup failure; wenzelm parents: 49098 diff changeset	429	case msg: PropertiesChanged =>
10e899bb6530 more permissive handling of plugin startup failure; wenzelm parents: 49098 diff changeset	430	Isabelle.setup_tooltips()
10e899bb6530 more permissive handling of plugin startup failure; wenzelm parents: 49098 diff changeset	431	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	432
49099 10e899bb6530 more permissive handling of plugin startup failure; wenzelm parents: 49098 diff changeset	433	case _ =>
10e899bb6530 more permissive handling of plugin startup failure; wenzelm parents: 49098 diff changeset	434	}
34318 c13e168a8ae6 original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout; wenzelm parents: diff changeset	435	}
c13e168a8ae6 original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout; wenzelm parents: diff changeset	436	}
c13e168a8ae6 original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout; wenzelm parents: diff changeset	437
34618 e45052ff7233 added Boolean_Property, Int_Property; wenzelm parents: 34615 diff changeset	438	override def start()
49099 10e899bb6530 more permissive handling of plugin startup failure; wenzelm parents: 49098 diff changeset	439	{
10e899bb6530 more permissive handling of plugin startup failure; wenzelm parents: 49098 diff changeset	440	try {
10e899bb6530 more permissive handling of plugin startup failure; wenzelm parents: 49098 diff changeset	441	Isabelle.plugin = this
10e899bb6530 more permissive handling of plugin startup failure; wenzelm parents: 49098 diff changeset	442	Isabelle_System.init()
10e899bb6530 more permissive handling of plugin startup failure; wenzelm parents: 49098 diff changeset	443	Isabelle_System.install_fonts()
10e899bb6530 more permissive handling of plugin startup failure; wenzelm parents: 49098 diff changeset	444
49245 cb70157293c0 manage Isabelle/jEdit options as Isabelle/Scala options (with persistent preferences); wenzelm parents: 49195 diff changeset	445	val init_options = Options.init()
cb70157293c0 manage Isabelle/jEdit options as Isabelle/Scala options (with persistent preferences); wenzelm parents: 49195 diff changeset	446	Swing_Thread.now {
cb70157293c0 manage Isabelle/jEdit options as Isabelle/Scala options (with persistent preferences); wenzelm parents: 49195 diff changeset	447	Isabelle.options.update(init_options)
cb70157293c0 manage Isabelle/jEdit options as Isabelle/Scala options (with persistent preferences); wenzelm parents: 49195 diff changeset	448	Isabelle.setup_tooltips()
cb70157293c0 manage Isabelle/jEdit options as Isabelle/Scala options (with persistent preferences); wenzelm parents: 49195 diff changeset	449	}
cb70157293c0 manage Isabelle/jEdit options as Isabelle/Scala options (with persistent preferences); wenzelm parents: 49195 diff changeset	450
49099 10e899bb6530 more permissive handling of plugin startup failure; wenzelm parents: 49098 diff changeset	451	SyntaxUtilities.setStyleExtender(new Token_Markup.Style_Extender)
10e899bb6530 more permissive handling of plugin startup failure; wenzelm parents: 49098 diff changeset	452	if (ModeProvider.instance.isInstanceOf[ModeProvider])
10e899bb6530 more permissive handling of plugin startup failure; wenzelm parents: 49098 diff changeset	453	ModeProvider.instance = new Token_Markup.Mode_Provider(ModeProvider.instance)
48870 4accee106f0f clarified initialization of Thy_Load, Thy_Info, Session; wenzelm parents: 48791 diff changeset	454
49099 10e899bb6530 more permissive handling of plugin startup failure; wenzelm parents: 49098 diff changeset	455	val content = Isabelle.session_content(false)
10e899bb6530 more permissive handling of plugin startup failure; wenzelm parents: 49098 diff changeset	456	val thy_load = new JEdit_Thy_Load(content.loaded_theories, content.syntax)
10e899bb6530 more permissive handling of plugin startup failure; wenzelm parents: 49098 diff changeset	457	Isabelle.session = new Session(thy_load)
48870 4accee106f0f clarified initialization of Thy_Load, Thy_Info, Session; wenzelm parents: 48791 diff changeset	458
49099 10e899bb6530 more permissive handling of plugin startup failure; wenzelm parents: 49098 diff changeset	459	Isabelle.session.phase_changed += session_manager
10e899bb6530 more permissive handling of plugin startup failure; wenzelm parents: 49098 diff changeset	460	Isabelle.startup_failure = None
10e899bb6530 more permissive handling of plugin startup failure; wenzelm parents: 49098 diff changeset	461	}
10e899bb6530 more permissive handling of plugin startup failure; wenzelm parents: 49098 diff changeset	462	catch {
10e899bb6530 more permissive handling of plugin startup failure; wenzelm parents: 49098 diff changeset	463	case exn: Throwable =>
10e899bb6530 more permissive handling of plugin startup failure; wenzelm parents: 49098 diff changeset	464	Isabelle.startup_failure = Some(exn)
10e899bb6530 more permissive handling of plugin startup failure; wenzelm parents: 49098 diff changeset	465	Isabelle.startup_notified = false
10e899bb6530 more permissive handling of plugin startup failure; wenzelm parents: 49098 diff changeset	466	}
34318 c13e168a8ae6 original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout; wenzelm parents: diff changeset	467	}
34618 e45052ff7233 added Boolean_Property, Int_Property; wenzelm parents: 34615 diff changeset	468
39628 f6e82967b5cd Plugin.stop: refrain from invalidating Isabelle.session -- some actors/dockables out there might still refer to it; wenzelm parents: 39518 diff changeset	469	override def stop()
34618 e45052ff7233 added Boolean_Property, Int_Property; wenzelm parents: 34615 diff changeset	470	{
49245 cb70157293c0 manage Isabelle/jEdit options as Isabelle/Scala options (with persistent preferences); wenzelm parents: 49195 diff changeset	471	if (Isabelle.startup_failure.isEmpty)
cb70157293c0 manage Isabelle/jEdit options as Isabelle/Scala options (with persistent preferences); wenzelm parents: 49195 diff changeset	472	Isabelle.options.value.save_prefs()
cb70157293c0 manage Isabelle/jEdit options as Isabelle/Scala options (with persistent preferences); wenzelm parents: 49195 diff changeset	473
49101 21c8d2070be9 continue with more robust dummy session after failed startup; wenzelm parents: 49100 diff changeset	474	Isabelle.session.phase_changed -= session_manager
21c8d2070be9 continue with more robust dummy session after failed startup; wenzelm parents: 49100 diff changeset	475	Isabelle.jedit_buffers.foreach(Isabelle.exit_model)
21c8d2070be9 continue with more robust dummy session after failed startup; wenzelm parents: 49100 diff changeset	476	Isabelle.session.stop()
34318 c13e168a8ae6 original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout; wenzelm parents: diff changeset	477	}
c13e168a8ae6 original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout; wenzelm parents: diff changeset	478	}

author	wenzelm
	Mon, 10 Sep 2012 15:20:50 +0200
changeset 49245	cb70157293c0
parent 49195	9d10bd85c1be
child 49246	248e66e8321f
permissions	-rw-r--r--