isabelle: src/Tools/jEdit/src/jedit/plugin.scala@105d1f112da5 (annotated)

36760 b82a698ef6c9 tuned headers; wenzelm parents: 36015 diff changeset	1	/* Title: Tools/jEdit/src/jedit/plugin.scala
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
34429 03afc73e185f tuned; wenzelm parents: 34422 diff changeset	12	import java.io.{FileInputStream, IOException}
34318 c13e168a8ae6 original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout; wenzelm parents: diff changeset	13	import java.awt.Font
34822 8c31275868cc tuned dialog; wenzelm parents: 34821 diff changeset	14	import javax.swing.JTextArea
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
34406 f81cd75ae331 restructured: independent provers in different buffers immler@in.tum.de parents: 34337 diff changeset	17
34429 03afc73e185f tuned; wenzelm parents: 34422 diff changeset	18	import org.gjt.sp.jedit.{jEdit, EBMessage, EBPlugin, Buffer, EditPane, ServiceManager, View}
34406 f81cd75ae331 restructured: independent provers in different buffers immler@in.tum.de parents: 34337 diff changeset	19	import org.gjt.sp.jedit.buffer.JEditBuffer
f81cd75ae331 restructured: independent provers in different buffers immler@in.tum.de parents: 34337 diff changeset	20	import org.gjt.sp.jedit.textarea.JEditTextArea
37557 1ae272fd4082 refresh Isabelle token marker after buffer properties changed, e.g. when fold mode is switched; wenzelm parents: 37241 diff changeset	21	import org.gjt.sp.jedit.msg.{BufferUpdate, EditPaneUpdate, PropertiesChanged}
37068 07936a4efe93 access statically typed dockable windows; wenzelm parents: 37019 diff changeset	22	import org.gjt.sp.jedit.gui.DockableWindowManager
34429 03afc73e185f tuned; wenzelm parents: 34422 diff changeset	23
34318 c13e168a8ae6 original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout; wenzelm parents: diff changeset	24
34618 e45052ff7233 added Boolean_Property, Int_Property; wenzelm parents: 34615 diff changeset	25	object Isabelle
e45052ff7233 added Boolean_Property, Int_Property; wenzelm parents: 34615 diff changeset	26	{
34784 02959dcea756 split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea); wenzelm parents: 34782 diff changeset	27	/* plugin instance */
02959dcea756 split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea); wenzelm parents: 34782 diff changeset	28
02959dcea756 split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea); wenzelm parents: 34782 diff changeset	29	var system: Isabelle_System = null
02959dcea756 split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea); wenzelm parents: 34782 diff changeset	30	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	31
02959dcea756 split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea); wenzelm parents: 34782 diff changeset	32
34618 e45052ff7233 added Boolean_Property, Int_Property; wenzelm parents: 34615 diff changeset	33	/* properties */
e45052ff7233 added Boolean_Property, Int_Property; wenzelm parents: 34615 diff changeset	34
e45052ff7233 added Boolean_Property, Int_Property; wenzelm parents: 34615 diff changeset	35	val OPTION_PREFIX = "options.isabelle."
e45052ff7233 added Boolean_Property, Int_Property; wenzelm parents: 34615 diff changeset	36
e45052ff7233 added Boolean_Property, Int_Property; wenzelm parents: 34615 diff changeset	37	object Property
e45052ff7233 added Boolean_Property, Int_Property; wenzelm parents: 34615 diff changeset	38	{
36814 dc85664dbf6d support Isabelle plugin properties with defaults; wenzelm parents: 36760 diff changeset	39	def apply(name: String): String =
dc85664dbf6d support Isabelle plugin properties with defaults; wenzelm parents: 36760 diff changeset	40	jEdit.getProperty(OPTION_PREFIX + name)
dc85664dbf6d support Isabelle plugin properties with defaults; wenzelm parents: 36760 diff changeset	41	def apply(name: String, default: String): String =
dc85664dbf6d support Isabelle plugin properties with defaults; wenzelm parents: 36760 diff changeset	42	jEdit.getProperty(OPTION_PREFIX + name, default)
dc85664dbf6d support Isabelle plugin properties with defaults; wenzelm parents: 36760 diff changeset	43	def update(name: String, value: String) =
dc85664dbf6d support Isabelle plugin properties with defaults; wenzelm parents: 36760 diff changeset	44	jEdit.setProperty(OPTION_PREFIX + name, value)
34468 9d4b4f290676 maintain Isabelle properties via object Isabelle.Property with apply/update methods; wenzelm parents: 34463 diff changeset	45	}
34433 3da749b53842 renamed Plugin.plugin to Plugin.self; wenzelm parents: 34429 diff changeset	46
34618 e45052ff7233 added Boolean_Property, Int_Property; wenzelm parents: 34615 diff changeset	47	object Boolean_Property
e45052ff7233 added Boolean_Property, Int_Property; wenzelm parents: 34615 diff changeset	48	{
36814 dc85664dbf6d support Isabelle plugin properties with defaults; wenzelm parents: 36760 diff changeset	49	def apply(name: String): Boolean =
dc85664dbf6d support Isabelle plugin properties with defaults; wenzelm parents: 36760 diff changeset	50	jEdit.getBooleanProperty(OPTION_PREFIX + name)
dc85664dbf6d support Isabelle plugin properties with defaults; wenzelm parents: 36760 diff changeset	51	def apply(name: String, default: Boolean): Boolean =
dc85664dbf6d support Isabelle plugin properties with defaults; wenzelm parents: 36760 diff changeset	52	jEdit.getBooleanProperty(OPTION_PREFIX + name, default)
dc85664dbf6d support Isabelle plugin properties with defaults; wenzelm parents: 36760 diff changeset	53	def update(name: String, value: Boolean) =
dc85664dbf6d support Isabelle plugin properties with defaults; wenzelm parents: 36760 diff changeset	54	jEdit.setBooleanProperty(OPTION_PREFIX + name, value)
34618 e45052ff7233 added Boolean_Property, Int_Property; wenzelm parents: 34615 diff changeset	55	}
e45052ff7233 added Boolean_Property, Int_Property; wenzelm parents: 34615 diff changeset	56
e45052ff7233 added Boolean_Property, Int_Property; wenzelm parents: 34615 diff changeset	57	object Int_Property
e45052ff7233 added Boolean_Property, Int_Property; wenzelm parents: 34615 diff changeset	58	{
36814 dc85664dbf6d support Isabelle plugin properties with defaults; wenzelm parents: 36760 diff changeset	59	def apply(name: String): Int =
dc85664dbf6d support Isabelle plugin properties with defaults; wenzelm parents: 36760 diff changeset	60	jEdit.getIntegerProperty(OPTION_PREFIX + name)
dc85664dbf6d support Isabelle plugin properties with defaults; wenzelm parents: 36760 diff changeset	61	def apply(name: String, default: Int): Int =
dc85664dbf6d support Isabelle plugin properties with defaults; wenzelm parents: 36760 diff changeset	62	jEdit.getIntegerProperty(OPTION_PREFIX + name, default)
dc85664dbf6d support Isabelle plugin properties with defaults; wenzelm parents: 36760 diff changeset	63	def update(name: String, value: Int) =
dc85664dbf6d support Isabelle plugin properties with defaults; wenzelm parents: 36760 diff changeset	64	jEdit.setIntegerProperty(OPTION_PREFIX + name, value)
34618 e45052ff7233 added Boolean_Property, Int_Property; wenzelm parents: 34615 diff changeset	65	}
e45052ff7233 added Boolean_Property, Int_Property; wenzelm parents: 34615 diff changeset	66
37164 8b4617ad1593 reuse main view.font from jEdit; wenzelm parents: 37068 diff changeset	67
8b4617ad1593 reuse main view.font from jEdit; wenzelm parents: 37068 diff changeset	68	/* font */
8b4617ad1593 reuse main view.font from jEdit; wenzelm parents: 37068 diff changeset	69
8b4617ad1593 reuse main view.font from jEdit; wenzelm parents: 37068 diff changeset	70	def font_family(): String = jEdit.getProperty("view.font")
8b4617ad1593 reuse main view.font from jEdit; wenzelm parents: 37068 diff changeset	71
37019 8f747cee4e27 zoom font size; wenzelm parents: 36814 diff changeset	72	def font_size(): Float =
8f747cee4e27 zoom font size; wenzelm parents: 36814 diff changeset	73	(jEdit.getIntegerProperty("view.fontsize", 16) *
8f747cee4e27 zoom font size; wenzelm parents: 36814 diff changeset	74	Int_Property("relative-font-size", 100)).toFloat / 100
36814 dc85664dbf6d support Isabelle plugin properties with defaults; wenzelm parents: 36760 diff changeset	75
34618 e45052ff7233 added Boolean_Property, Int_Property; wenzelm parents: 34615 diff changeset	76
37201 8517a650cfdc control tooltip font via Swing HTML, with tooltip-font-size property; wenzelm parents: 37177 diff changeset	77	/* tooltip markup */
8517a650cfdc control tooltip font via Swing HTML, with tooltip-font-size property; wenzelm parents: 37177 diff changeset	78
8517a650cfdc control tooltip font via Swing HTML, with tooltip-font-size property; wenzelm parents: 37177 diff changeset	79	def tooltip(text: String): String =
37203 c4261f3bbdd7 more flexibile font size via CSS <style> instead of old <font> element; wenzelm parents: 37201 diff changeset	80	"<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	81	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	82	HTML.encode(text) + "</pre></html>"
37201 8517a650cfdc control tooltip font via Swing HTML, with tooltip-font-size property; wenzelm parents: 37177 diff changeset	83
8517a650cfdc control tooltip font via Swing HTML, with tooltip-font-size property; wenzelm parents: 37177 diff changeset	84
34618 e45052ff7233 added Boolean_Property, Int_Property; wenzelm parents: 34615 diff changeset	85	/* settings */
e45052ff7233 added Boolean_Property, Int_Property; wenzelm parents: 34615 diff changeset	86
34782 fcd6a41326a6 refined treatment of default logic concerning property and GUI; wenzelm parents: 34781 diff changeset	87	def default_logic(): String =
fcd6a41326a6 refined treatment of default logic concerning property and GUI; wenzelm parents: 34781 diff changeset	88	{
fcd6a41326a6 refined treatment of default logic concerning property and GUI; wenzelm parents: 34781 diff changeset	89	val logic = system.getenv("JEDIT_LOGIC")
fcd6a41326a6 refined treatment of default logic concerning property and GUI; wenzelm parents: 34781 diff changeset	90	if (logic != "") logic
fcd6a41326a6 refined treatment of default logic concerning property and GUI; wenzelm parents: 34781 diff changeset	91	else system.getenv_strict("ISABELLE_LOGIC")
fcd6a41326a6 refined treatment of default logic concerning property and GUI; wenzelm parents: 34781 diff changeset	92	}
fcd6a41326a6 refined treatment of default logic concerning property and GUI; wenzelm parents: 34781 diff changeset	93
fcd6a41326a6 refined treatment of default logic concerning property and GUI; wenzelm parents: 34781 diff changeset	94	def isabelle_args(): List[String] =
34618 e45052ff7233 added Boolean_Property, Int_Property; wenzelm parents: 34615 diff changeset	95	{
34780 d0ff1c3a91ea more serious command line handling; wenzelm parents: 34779 diff changeset	96	val modes = system.getenv("JEDIT_PRINT_MODE").split(",").toList.map("-m" + _)
d0ff1c3a91ea more serious command line handling; wenzelm parents: 34779 diff changeset	97	val logic = {
34784 02959dcea756 split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea); wenzelm parents: 34782 diff changeset	98	val logic = Property("logic")
34782 fcd6a41326a6 refined treatment of default logic concerning property and GUI; wenzelm parents: 34781 diff changeset	99	if (logic != null && logic != "") logic
fcd6a41326a6 refined treatment of default logic concerning property and GUI; wenzelm parents: 34781 diff changeset	100	else default_logic()
34780 d0ff1c3a91ea more serious command line handling; wenzelm parents: 34779 diff changeset	101	}
d0ff1c3a91ea more serious command line handling; wenzelm parents: 34779 diff changeset	102	modes ++ List(logic)
34502 7d1d13750890 added Isabelle.default_logic; wenzelm parents: 34497 diff changeset	103	}
7d1d13750890 added Isabelle.default_logic; wenzelm parents: 34497 diff changeset	104
34618 e45052ff7233 added Boolean_Property, Int_Property; wenzelm parents: 34615 diff changeset	105
38221 e0f00f0945b4 misc tuning and clarification; wenzelm parents: 37557 diff changeset	106	/* 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	107
37177 17331ca75044 avoid deprecated Iterator.fromArray; wenzelm parents: 37164 diff changeset	108	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	109
37177 17331ca75044 avoid deprecated Iterator.fromArray; wenzelm parents: 37164 diff changeset	110	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	111
02959dcea756 split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea); wenzelm parents: 34782 diff changeset	112	def jedit_text_areas(view: View): Iterator[JEditTextArea] =
37177 17331ca75044 avoid deprecated Iterator.fromArray; wenzelm parents: 37164 diff changeset	113	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	114
02959dcea756 split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea); wenzelm parents: 34782 diff changeset	115	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	116	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	117
02959dcea756 split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea); wenzelm parents: 34782 diff changeset	118	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	119	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	120
38640 105d1f112da5 sporadic locking of jEdit buffer; wenzelm parents: 38222 diff changeset	121	def buffer_read_lock[A](buffer: JEditBuffer)(body: => A): A =
105d1f112da5 sporadic locking of jEdit buffer; wenzelm parents: 38222 diff changeset	122	{
105d1f112da5 sporadic locking of jEdit buffer; wenzelm parents: 38222 diff changeset	123	try { buffer.readLock(); body }
105d1f112da5 sporadic locking of jEdit buffer; wenzelm parents: 38222 diff changeset	124	finally { buffer.readUnlock() }
105d1f112da5 sporadic locking of jEdit buffer; wenzelm parents: 38222 diff changeset	125	}
105d1f112da5 sporadic locking of jEdit buffer; wenzelm parents: 38222 diff changeset	126
34784 02959dcea756 split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea); wenzelm parents: 34782 diff changeset	127
37068 07936a4efe93 access statically typed dockable windows; wenzelm parents: 37019 diff changeset	128	/* dockable windows */
07936a4efe93 access statically typed dockable windows; wenzelm parents: 37019 diff changeset	129
07936a4efe93 access statically typed dockable windows; wenzelm parents: 37019 diff changeset	130	private def wm(view: View): DockableWindowManager = view.getDockableWindowManager
07936a4efe93 access statically typed dockable windows; wenzelm parents: 37019 diff changeset	131
07936a4efe93 access statically typed dockable windows; wenzelm parents: 37019 diff changeset	132	def docked_output(view: View): Option[Output_Dockable] =
07936a4efe93 access statically typed dockable windows; wenzelm parents: 37019 diff changeset	133	wm(view).getDockableWindow("isabelle-output") match {
07936a4efe93 access statically typed dockable windows; wenzelm parents: 37019 diff changeset	134	case dockable: Output_Dockable => Some(dockable)
07936a4efe93 access statically typed dockable windows; wenzelm parents: 37019 diff changeset	135	case _ => None
07936a4efe93 access statically typed dockable windows; wenzelm parents: 37019 diff changeset	136	}
07936a4efe93 access statically typed dockable windows; wenzelm parents: 37019 diff changeset	137
07936a4efe93 access statically typed dockable windows; wenzelm parents: 37019 diff changeset	138	def docked_raw_output(view: View): Option[Raw_Output_Dockable] =
07936a4efe93 access statically typed dockable windows; wenzelm parents: 37019 diff changeset	139	wm(view).getDockableWindow("isabelle-raw-output") match {
07936a4efe93 access statically typed dockable windows; wenzelm parents: 37019 diff changeset	140	case dockable: Raw_Output_Dockable => Some(dockable)
07936a4efe93 access statically typed dockable windows; wenzelm parents: 37019 diff changeset	141	case _ => None
07936a4efe93 access statically typed dockable windows; wenzelm parents: 37019 diff changeset	142	}
07936a4efe93 access statically typed dockable windows; wenzelm parents: 37019 diff changeset	143
07936a4efe93 access statically typed dockable windows; wenzelm parents: 37019 diff changeset	144	def docked_protocol(view: View): Option[Protocol_Dockable] =
07936a4efe93 access statically typed dockable windows; wenzelm parents: 37019 diff changeset	145	wm(view).getDockableWindow("isabelle-protocol") match {
07936a4efe93 access statically typed dockable windows; wenzelm parents: 37019 diff changeset	146	case dockable: Protocol_Dockable => Some(dockable)
07936a4efe93 access statically typed dockable windows; wenzelm parents: 37019 diff changeset	147	case _ => None
07936a4efe93 access statically typed dockable windows; wenzelm parents: 37019 diff changeset	148	}
07936a4efe93 access statically typed dockable windows; wenzelm parents: 37019 diff changeset	149
07936a4efe93 access statically typed dockable windows; wenzelm parents: 37019 diff changeset	150
38221 e0f00f0945b4 misc tuning and clarification; wenzelm parents: 37557 diff changeset	151	/* manage prover */ // FIXME async!?
34820 a8ba6cde13e9 basic setup for synchronous / modal (!) prover startup; wenzelm parents: 34808 diff changeset	152
a8ba6cde13e9 basic setup for synchronous / modal (!) prover startup; wenzelm parents: 34808 diff changeset	153	private def prover_started(view: View): Boolean =
a8ba6cde13e9 basic setup for synchronous / modal (!) prover startup; wenzelm parents: 34808 diff changeset	154	{
a8ba6cde13e9 basic setup for synchronous / modal (!) prover startup; wenzelm parents: 34808 diff changeset	155	val timeout = Int_Property("startup-timeout") max 1000
38221 e0f00f0945b4 misc tuning and clarification; wenzelm parents: 37557 diff changeset	156	session.started(timeout, Isabelle.isabelle_args()) match {
34820 a8ba6cde13e9 basic setup for synchronous / modal (!) prover startup; wenzelm parents: 34808 diff changeset	157	case Some(err) =>
34822 8c31275868cc tuned dialog; wenzelm parents: 34821 diff changeset	158	val text = new JTextArea(err); text.setEditable(false)
8c31275868cc tuned dialog; wenzelm parents: 34821 diff changeset	159	Library.error_dialog(view, null, "Failed to start Isabelle process", text)
34820 a8ba6cde13e9 basic setup for synchronous / modal (!) prover startup; wenzelm parents: 34808 diff changeset	160	false
a8ba6cde13e9 basic setup for synchronous / modal (!) prover startup; wenzelm parents: 34808 diff changeset	161	case None => true
a8ba6cde13e9 basic setup for synchronous / modal (!) prover startup; wenzelm parents: 34808 diff changeset	162	}
a8ba6cde13e9 basic setup for synchronous / modal (!) prover startup; wenzelm parents: 34808 diff changeset	163	}
a8ba6cde13e9 basic setup for synchronous / modal (!) prover startup; wenzelm parents: 34808 diff changeset	164
a8ba6cde13e9 basic setup for synchronous / modal (!) prover startup; wenzelm parents: 34808 diff changeset	165
34784 02959dcea756 split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea); wenzelm parents: 34782 diff changeset	166	/* activation */
02959dcea756 split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea); wenzelm parents: 34782 diff changeset	167
34820 a8ba6cde13e9 basic setup for synchronous / modal (!) prover startup; wenzelm parents: 34808 diff changeset	168	def activate_buffer(view: View, buffer: Buffer)
34784 02959dcea756 split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea); wenzelm parents: 34782 diff changeset	169	{
34820 a8ba6cde13e9 basic setup for synchronous / modal (!) prover startup; wenzelm parents: 34808 diff changeset	170	if (prover_started(view)) {
38222 dac5fa0ac971 replaced individual Document_Model history by all-inclusive one in Session; wenzelm parents: 38221 diff changeset	171	// FIXME proper error handling
dac5fa0ac971 replaced individual Document_Model history by all-inclusive one in Session; wenzelm parents: 38221 diff changeset	172	val (_, thy_name) = Thy_Header.split_thy_path(Isabelle.system.posix_path(buffer.getPath))
dac5fa0ac971 replaced individual Document_Model history by all-inclusive one in Session; wenzelm parents: 38221 diff changeset	173
dac5fa0ac971 replaced individual Document_Model history by all-inclusive one in Session; wenzelm parents: 38221 diff changeset	174	val model = Document_Model.init(session, buffer, thy_name)
34820 a8ba6cde13e9 basic setup for synchronous / modal (!) prover startup; wenzelm parents: 34808 diff changeset	175	for (text_area <- jedit_text_areas(buffer))
a8ba6cde13e9 basic setup for synchronous / modal (!) prover startup; wenzelm parents: 34808 diff changeset	176	Document_View.init(model, text_area)
a8ba6cde13e9 basic setup for synchronous / modal (!) prover startup; wenzelm parents: 34808 diff changeset	177	}
34784 02959dcea756 split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea); wenzelm parents: 34782 diff changeset	178	}
02959dcea756 split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea); wenzelm parents: 34782 diff changeset	179
02959dcea756 split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea); wenzelm parents: 34782 diff changeset	180	def deactivate_buffer(buffer: Buffer)
02959dcea756 split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea); wenzelm parents: 34782 diff changeset	181	{
02959dcea756 split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea); wenzelm parents: 34782 diff changeset	182	session.stop() // FIXME not yet
02959dcea756 split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea); wenzelm parents: 34782 diff changeset	183
02959dcea756 split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea); wenzelm parents: 34782 diff changeset	184	for (text_area <- jedit_text_areas(buffer))
02959dcea756 split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea); wenzelm parents: 34782 diff changeset	185	Document_View.exit(text_area)
02959dcea756 split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea); wenzelm parents: 34782 diff changeset	186	Document_Model.exit(buffer)
02959dcea756 split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea); wenzelm parents: 34782 diff changeset	187	}
02959dcea756 split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea); wenzelm parents: 34782 diff changeset	188
02959dcea756 split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea); wenzelm parents: 34782 diff changeset	189	def switch_active(view: View) =
02959dcea756 split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea); wenzelm parents: 34782 diff changeset	190	{
02959dcea756 split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea); wenzelm parents: 34782 diff changeset	191	val buffer = view.getBuffer
34788 3779c54a2d21 direct apply for Document_Model and Document_View; wenzelm parents: 34787 diff changeset	192	if (Document_Model(buffer).isDefined) deactivate_buffer(buffer)
34820 a8ba6cde13e9 basic setup for synchronous / modal (!) prover startup; wenzelm parents: 34808 diff changeset	193	else activate_buffer(view, buffer)
34784 02959dcea756 split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea); wenzelm parents: 34782 diff changeset	194	}
02959dcea756 split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea); wenzelm parents: 34782 diff changeset	195
02959dcea756 split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea); wenzelm parents: 34782 diff changeset	196	def is_active(view: View): Boolean =
34788 3779c54a2d21 direct apply for Document_Model and Document_View; wenzelm parents: 34787 diff changeset	197	Document_Model(view.getBuffer).isDefined
34318 c13e168a8ae6 original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout; wenzelm parents: diff changeset	198	}
c13e168a8ae6 original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout; wenzelm parents: diff changeset	199
34429 03afc73e185f tuned; wenzelm parents: 34422 diff changeset	200
34618 e45052ff7233 added Boolean_Property, Int_Property; wenzelm parents: 34615 diff changeset	201	class Plugin extends EBPlugin
e45052ff7233 added Boolean_Property, Int_Property; wenzelm parents: 34615 diff changeset	202	{
e45052ff7233 added Boolean_Property, Int_Property; wenzelm parents: 34615 diff changeset	203	/* main plugin plumbing */
34433 3da749b53842 renamed Plugin.plugin to Plugin.self; wenzelm parents: 34429 diff changeset	204
34767 8dd19c5f8c56 added properties_changed event bus; wenzelm parents: 34764 diff changeset	205	override def handleMessage(message: EBMessage)
34618 e45052ff7233 added Boolean_Property, Int_Property; wenzelm parents: 34615 diff changeset	206	{
34767 8dd19c5f8c56 added properties_changed event bus; wenzelm parents: 34764 diff changeset	207	message match {
37557 1ae272fd4082 refresh Isabelle token marker after buffer properties changed, e.g. when fold mode is switched; wenzelm parents: 37241 diff changeset	208	case msg: BufferUpdate
1ae272fd4082 refresh Isabelle token marker after buffer properties changed, e.g. when fold mode is switched; wenzelm parents: 37241 diff changeset	209	if msg.getWhat == BufferUpdate.PROPERTIES_CHANGED =>
1ae272fd4082 refresh Isabelle token marker after buffer properties changed, e.g. when fold mode is switched; wenzelm parents: 37241 diff changeset	210	Document_Model(msg.getBuffer) match {
1ae272fd4082 refresh Isabelle token marker after buffer properties changed, e.g. when fold mode is switched; wenzelm parents: 37241 diff changeset	211	case Some(model) => model.refresh()
1ae272fd4082 refresh Isabelle token marker after buffer properties changed, e.g. when fold mode is switched; wenzelm parents: 37241 diff changeset	212	case _ =>
1ae272fd4082 refresh Isabelle token marker after buffer properties changed, e.g. when fold mode is switched; wenzelm parents: 37241 diff changeset	213	}
1ae272fd4082 refresh Isabelle token marker after buffer properties changed, e.g. when fold mode is switched; wenzelm parents: 37241 diff changeset	214
34767 8dd19c5f8c56 added properties_changed event bus; wenzelm parents: 34764 diff changeset	215	case msg: EditPaneUpdate =>
34784 02959dcea756 split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea); wenzelm parents: 34782 diff changeset	216	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	217	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	218	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	219
34787 0feac35069c6 need to handle EditPaneUpdate.CREATED explicitly, not included in EditPaneUpdate.BUFFER_CHANGED; wenzelm parents: 34784 diff changeset	220	def init_view()
0feac35069c6 need to handle EditPaneUpdate.CREATED explicitly, not included in EditPaneUpdate.BUFFER_CHANGED; wenzelm parents: 34784 diff changeset	221	{
34788 3779c54a2d21 direct apply for Document_Model and Document_View; wenzelm parents: 34787 diff changeset	222	Document_Model(buffer) match {
34787 0feac35069c6 need to handle EditPaneUpdate.CREATED explicitly, not included in EditPaneUpdate.BUFFER_CHANGED; wenzelm parents: 34784 diff changeset	223	case Some(model) => Document_View.init(model, text_area)
0feac35069c6 need to handle EditPaneUpdate.CREATED explicitly, not included in EditPaneUpdate.BUFFER_CHANGED; wenzelm parents: 34784 diff changeset	224	case None =>
0feac35069c6 need to handle EditPaneUpdate.CREATED explicitly, not included in EditPaneUpdate.BUFFER_CHANGED; wenzelm parents: 34784 diff changeset	225	}
0feac35069c6 need to handle EditPaneUpdate.CREATED explicitly, not included in EditPaneUpdate.BUFFER_CHANGED; wenzelm parents: 34784 diff changeset	226	}
0feac35069c6 need to handle EditPaneUpdate.CREATED explicitly, not included in EditPaneUpdate.BUFFER_CHANGED; wenzelm parents: 34784 diff changeset	227	def exit_view()
0feac35069c6 need to handle EditPaneUpdate.CREATED explicitly, not included in EditPaneUpdate.BUFFER_CHANGED; wenzelm parents: 34784 diff changeset	228	{
34788 3779c54a2d21 direct apply for Document_Model and Document_View; wenzelm parents: 34787 diff changeset	229	if (Document_View(text_area).isDefined)
34787 0feac35069c6 need to handle EditPaneUpdate.CREATED explicitly, not included in EditPaneUpdate.BUFFER_CHANGED; wenzelm parents: 34784 diff changeset	230	Document_View.exit(text_area)
0feac35069c6 need to handle EditPaneUpdate.CREATED explicitly, not included in EditPaneUpdate.BUFFER_CHANGED; wenzelm parents: 34784 diff changeset	231	}
34767 8dd19c5f8c56 added properties_changed event bus; wenzelm parents: 34764 diff changeset	232	msg.getWhat match {
34787 0feac35069c6 need to handle EditPaneUpdate.CREATED explicitly, not included in EditPaneUpdate.BUFFER_CHANGED; wenzelm parents: 34784 diff changeset	233	case EditPaneUpdate.BUFFER_CHANGED => exit_view(); init_view()
0feac35069c6 need to handle EditPaneUpdate.CREATED explicitly, not included in EditPaneUpdate.BUFFER_CHANGED; wenzelm parents: 34784 diff changeset	234	case EditPaneUpdate.CREATED => init_view()
0feac35069c6 need to handle EditPaneUpdate.CREATED explicitly, not included in EditPaneUpdate.BUFFER_CHANGED; wenzelm parents: 34784 diff changeset	235	case EditPaneUpdate.DESTROYED => exit_view()
34671 d179fcb04cbc output_info specific to prover immler@in.tum.de parents: 34670 diff changeset	236	case _ =>
d179fcb04cbc output_info specific to prover immler@in.tum.de parents: 34670 diff changeset	237	}
34784 02959dcea756 split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea); wenzelm parents: 34782 diff changeset	238
34777 91d6089cef88 class Session models full session, with or without prover process (cf. heaps, browser_info); wenzelm parents: 34774 diff changeset	239	case msg: PropertiesChanged =>
37241 04d2521e79b0 basic support for sub/superscript token markup -- NB: need to maintain extended token types eagerly, since jEdit occasionally reinstalls a style array that is too short; wenzelm parents: 37203 diff changeset	240	Swing_Thread.now {
04d2521e79b0 basic support for sub/superscript token markup -- NB: need to maintain extended token types eagerly, since jEdit occasionally reinstalls a style array that is too short; wenzelm parents: 37203 diff changeset	241	for (text_area <- Isabelle.jedit_text_areas if Document_View(text_area).isDefined)
04d2521e79b0 basic support for sub/superscript token markup -- NB: need to maintain extended token types eagerly, since jEdit occasionally reinstalls a style array that is too short; wenzelm parents: 37203 diff changeset	242	Document_View(text_area).get.extend_styles()
04d2521e79b0 basic support for sub/superscript token markup -- NB: need to maintain extended token types eagerly, since jEdit occasionally reinstalls a style array that is too short; wenzelm parents: 37203 diff changeset	243	}
04d2521e79b0 basic support for sub/superscript token markup -- NB: need to maintain extended token types eagerly, since jEdit occasionally reinstalls a style array that is too short; wenzelm parents: 37203 diff changeset	244
34791 b97d5b38dea4 explicit object Session.Global_Settings; wenzelm parents: 34788 diff changeset	245	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	246
34318 c13e168a8ae6 original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout; wenzelm parents: diff changeset	247	case _ =>
c13e168a8ae6 original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout; wenzelm parents: diff changeset	248	}
c13e168a8ae6 original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout; wenzelm parents: diff changeset	249	}
c13e168a8ae6 original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout; wenzelm parents: diff changeset	250
34618 e45052ff7233 added Boolean_Property, Int_Property; wenzelm parents: 34615 diff changeset	251	override def start()
e45052ff7233 added Boolean_Property, Int_Property; wenzelm parents: 34615 diff changeset	252	{
34615 5e61055bf35b renamed IsabelleProcess to Isabelle_Process; wenzelm parents: 34612 diff changeset	253	Isabelle.system = new Isabelle_System
34774 1fa466333361 install_fonts; wenzelm parents: 34772 diff changeset	254	Isabelle.system.install_fonts()
34777 91d6089cef88 class Session models full session, with or without prover process (cf. heaps, browser_info); wenzelm parents: 34774 diff changeset	255	Isabelle.session = new Session(Isabelle.system) // FIXME dialog!?
34318 c13e168a8ae6 original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout; wenzelm parents: diff changeset	256	}
34618 e45052ff7233 added Boolean_Property, Int_Property; wenzelm parents: 34615 diff changeset	257
e45052ff7233 added Boolean_Property, Int_Property; wenzelm parents: 34615 diff changeset	258	override def stop()
e45052ff7233 added Boolean_Property, Int_Property; wenzelm parents: 34615 diff changeset	259	{
34777 91d6089cef88 class Session models full session, with or without prover process (cf. heaps, browser_info); wenzelm parents: 34774 diff changeset	260	Isabelle.session.stop() // FIXME dialog!?
91d6089cef88 class Session models full session, with or without prover process (cf. heaps, browser_info); wenzelm parents: 34774 diff changeset	261	Isabelle.session = null
34441 ff3b7ae2b12a replaced static IsabelleSystem by Isabelle.system; wenzelm parents: 34440 diff changeset	262	Isabelle.system = null
34318 c13e168a8ae6 original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout; wenzelm parents: diff changeset	263	}
c13e168a8ae6 original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout; wenzelm parents: diff changeset	264	}

author	wenzelm
	Mon, 23 Aug 2010 17:35:47 +0200
changeset 38640	105d1f112da5
parent 38222	dac5fa0ac971
child 38843	d95522496593
permissions	-rw-r--r--