isabelle: src/Tools/jEdit/src/jedit/plugin.scala@44181423183a (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
c13e168a8ae6 original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout; wenzelm parents: diff changeset	14
34497 184fda8cce04 more explicit indication of mutable collections; wenzelm parents: 34487 diff changeset	15	import scala.collection.mutable
39517 e036c67448e6 separate Isabelle.logic_selector; wenzelm parents: 39515 diff changeset	16	import scala.swing.ComboBox
34406 f81cd75ae331 restructured: independent provers in different buffers immler@in.tum.de parents: 34337 diff changeset	17
39241 e9a442606db3 Isabelle.load_icon with some sanity checks; wenzelm parents: 39167 diff changeset	18	import org.gjt.sp.jedit.{jEdit, GUIUtilities, EBMessage, EBPlugin,
e9a442606db3 Isabelle.load_icon with some sanity checks; wenzelm parents: 39167 diff changeset	19	Buffer, EditPane, ServiceManager, View}
34406 f81cd75ae331 restructured: independent provers in different buffers immler@in.tum.de parents: 34337 diff changeset	20	import org.gjt.sp.jedit.buffer.JEditBuffer
39043 a0d7e9b580ec added gfx_range convenience; wenzelm parents: 38854 diff changeset	21	import org.gjt.sp.jedit.textarea.{JEditTextArea, TextArea}
39630 44181423183a explicit Session.Phase indication with associated event bus; wenzelm parents: 39628 diff changeset	22	import org.gjt.sp.jedit.msg.{BufferUpdate, EditPaneUpdate, PropertiesChanged, ViewUpdate}
37068 07936a4efe93 access statically typed dockable windows; wenzelm parents: 37019 diff changeset	23	import org.gjt.sp.jedit.gui.DockableWindowManager
34429 03afc73e185f tuned; wenzelm parents: 34422 diff changeset	24
39241 e9a442606db3 Isabelle.load_icon with some sanity checks; wenzelm parents: 39167 diff changeset	25	import org.gjt.sp.util.Log
e9a442606db3 Isabelle.load_icon with some sanity checks; wenzelm parents: 39167 diff changeset	26
39630 44181423183a explicit Session.Phase indication with associated event bus; wenzelm parents: 39628 diff changeset	27	import scala.actors.Actor
44181423183a explicit Session.Phase indication with associated event bus; wenzelm parents: 39628 diff changeset	28	import Actor._
44181423183a explicit Session.Phase indication with associated event bus; wenzelm parents: 39628 diff changeset	29
34318 c13e168a8ae6 original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout; wenzelm parents: diff changeset	30
34618 e45052ff7233 added Boolean_Property, Int_Property; wenzelm parents: 34615 diff changeset	31	object Isabelle
e45052ff7233 added Boolean_Property, Int_Property; wenzelm parents: 34615 diff changeset	32	{
34784 02959dcea756 split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea); wenzelm parents: 34782 diff changeset	33	/* plugin instance */
02959dcea756 split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea); wenzelm parents: 34782 diff changeset	34
02959dcea756 split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea); wenzelm parents: 34782 diff changeset	35	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	36	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	37
02959dcea756 split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea); wenzelm parents: 34782 diff changeset	38
34618 e45052ff7233 added Boolean_Property, Int_Property; wenzelm parents: 34615 diff changeset	39	/* properties */
e45052ff7233 added Boolean_Property, Int_Property; wenzelm parents: 34615 diff changeset	40
e45052ff7233 added Boolean_Property, Int_Property; wenzelm parents: 34615 diff changeset	41	val OPTION_PREFIX = "options.isabelle."
e45052ff7233 added Boolean_Property, Int_Property; wenzelm parents: 34615 diff changeset	42
e45052ff7233 added Boolean_Property, Int_Property; wenzelm parents: 34615 diff changeset	43	object Property
e45052ff7233 added Boolean_Property, Int_Property; wenzelm parents: 34615 diff changeset	44	{
36814 dc85664dbf6d support Isabelle plugin properties with defaults; wenzelm parents: 36760 diff changeset	45	def apply(name: String): String =
dc85664dbf6d support Isabelle plugin properties with defaults; wenzelm parents: 36760 diff changeset	46	jEdit.getProperty(OPTION_PREFIX + name)
dc85664dbf6d support Isabelle plugin properties with defaults; wenzelm parents: 36760 diff changeset	47	def apply(name: String, default: String): String =
dc85664dbf6d support Isabelle plugin properties with defaults; wenzelm parents: 36760 diff changeset	48	jEdit.getProperty(OPTION_PREFIX + name, default)
dc85664dbf6d support Isabelle plugin properties with defaults; wenzelm parents: 36760 diff changeset	49	def update(name: String, value: String) =
dc85664dbf6d support Isabelle plugin properties with defaults; wenzelm parents: 36760 diff changeset	50	jEdit.setProperty(OPTION_PREFIX + name, value)
34468 9d4b4f290676 maintain Isabelle properties via object Isabelle.Property with apply/update methods; wenzelm parents: 34463 diff changeset	51	}
34433 3da749b53842 renamed Plugin.plugin to Plugin.self; wenzelm parents: 34429 diff changeset	52
34618 e45052ff7233 added Boolean_Property, Int_Property; wenzelm parents: 34615 diff changeset	53	object Boolean_Property
e45052ff7233 added Boolean_Property, Int_Property; wenzelm parents: 34615 diff changeset	54	{
36814 dc85664dbf6d support Isabelle plugin properties with defaults; wenzelm parents: 36760 diff changeset	55	def apply(name: String): Boolean =
dc85664dbf6d support Isabelle plugin properties with defaults; wenzelm parents: 36760 diff changeset	56	jEdit.getBooleanProperty(OPTION_PREFIX + name)
dc85664dbf6d support Isabelle plugin properties with defaults; wenzelm parents: 36760 diff changeset	57	def apply(name: String, default: Boolean): Boolean =
dc85664dbf6d support Isabelle plugin properties with defaults; wenzelm parents: 36760 diff changeset	58	jEdit.getBooleanProperty(OPTION_PREFIX + name, default)
dc85664dbf6d support Isabelle plugin properties with defaults; wenzelm parents: 36760 diff changeset	59	def update(name: String, value: Boolean) =
dc85664dbf6d support Isabelle plugin properties with defaults; wenzelm parents: 36760 diff changeset	60	jEdit.setBooleanProperty(OPTION_PREFIX + name, value)
34618 e45052ff7233 added Boolean_Property, Int_Property; wenzelm parents: 34615 diff changeset	61	}
e45052ff7233 added Boolean_Property, Int_Property; wenzelm parents: 34615 diff changeset	62
e45052ff7233 added Boolean_Property, Int_Property; wenzelm parents: 34615 diff changeset	63	object Int_Property
e45052ff7233 added Boolean_Property, Int_Property; wenzelm parents: 34615 diff changeset	64	{
36814 dc85664dbf6d support Isabelle plugin properties with defaults; wenzelm parents: 36760 diff changeset	65	def apply(name: String): Int =
dc85664dbf6d support Isabelle plugin properties with defaults; wenzelm parents: 36760 diff changeset	66	jEdit.getIntegerProperty(OPTION_PREFIX + name)
dc85664dbf6d support Isabelle plugin properties with defaults; wenzelm parents: 36760 diff changeset	67	def apply(name: String, default: Int): Int =
dc85664dbf6d support Isabelle plugin properties with defaults; wenzelm parents: 36760 diff changeset	68	jEdit.getIntegerProperty(OPTION_PREFIX + name, default)
dc85664dbf6d support Isabelle plugin properties with defaults; wenzelm parents: 36760 diff changeset	69	def update(name: String, value: Int) =
dc85664dbf6d support Isabelle plugin properties with defaults; wenzelm parents: 36760 diff changeset	70	jEdit.setIntegerProperty(OPTION_PREFIX + name, value)
34618 e45052ff7233 added Boolean_Property, Int_Property; wenzelm parents: 34615 diff changeset	71	}
e45052ff7233 added Boolean_Property, Int_Property; wenzelm parents: 34615 diff changeset	72
37164 8b4617ad1593 reuse main view.font from jEdit; wenzelm parents: 37068 diff changeset	73
8b4617ad1593 reuse main view.font from jEdit; wenzelm parents: 37068 diff changeset	74	/* font */
8b4617ad1593 reuse main view.font from jEdit; wenzelm parents: 37068 diff changeset	75
8b4617ad1593 reuse main view.font from jEdit; wenzelm parents: 37068 diff changeset	76	def font_family(): String = jEdit.getProperty("view.font")
8b4617ad1593 reuse main view.font from jEdit; wenzelm parents: 37068 diff changeset	77
37019 8f747cee4e27 zoom font size; wenzelm parents: 36814 diff changeset	78	def font_size(): Float =
8f747cee4e27 zoom font size; wenzelm parents: 36814 diff changeset	79	(jEdit.getIntegerProperty("view.fontsize", 16) *
8f747cee4e27 zoom font size; wenzelm parents: 36814 diff changeset	80	Int_Property("relative-font-size", 100)).toFloat / 100
36814 dc85664dbf6d support Isabelle plugin properties with defaults; wenzelm parents: 36760 diff changeset	81
34618 e45052ff7233 added Boolean_Property, Int_Property; wenzelm parents: 34615 diff changeset	82
39043 a0d7e9b580ec added gfx_range convenience; wenzelm parents: 38854 diff changeset	83	/* text area ranges */
a0d7e9b580ec added gfx_range convenience; wenzelm parents: 38854 diff changeset	84
a0d7e9b580ec added gfx_range convenience; wenzelm parents: 38854 diff changeset	85	case class Gfx_Range(val x: Int, val y: Int, val length: Int)
a0d7e9b580ec added gfx_range convenience; wenzelm parents: 38854 diff changeset	86
a0d7e9b580ec added gfx_range convenience; wenzelm parents: 38854 diff changeset	87	def gfx_range(text_area: TextArea, range: Text.Range): Option[Gfx_Range] =
a0d7e9b580ec added gfx_range convenience; wenzelm parents: 38854 diff changeset	88	{
a0d7e9b580ec added gfx_range convenience; wenzelm parents: 38854 diff changeset	89	val p = text_area.offsetToXY(range.start)
a0d7e9b580ec added gfx_range convenience; wenzelm parents: 38854 diff changeset	90	val q = text_area.offsetToXY(range.stop)
a0d7e9b580ec added gfx_range convenience; wenzelm parents: 38854 diff changeset	91	if (p != null && q != null && p.y == q.y) Some(new Gfx_Range(p.x, p.y, q.x - p.x))
a0d7e9b580ec added gfx_range convenience; wenzelm parents: 38854 diff changeset	92	else None
a0d7e9b580ec added gfx_range convenience; wenzelm parents: 38854 diff changeset	93	}
a0d7e9b580ec added gfx_range convenience; wenzelm parents: 38854 diff changeset	94
a0d7e9b580ec added gfx_range convenience; wenzelm parents: 38854 diff changeset	95
37201 8517a650cfdc control tooltip font via Swing HTML, with tooltip-font-size property; wenzelm parents: 37177 diff changeset	96	/* tooltip markup */
8517a650cfdc control tooltip font via Swing HTML, with tooltip-font-size property; wenzelm parents: 37177 diff changeset	97
8517a650cfdc control tooltip font via Swing HTML, with tooltip-font-size property; wenzelm parents: 37177 diff changeset	98	def tooltip(text: String): String =
37203 c4261f3bbdd7 more flexibile font size via CSS <style> instead of old <font> element; wenzelm parents: 37201 diff changeset	99	"<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	100	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	101	HTML.encode(text) + "</pre></html>"
37201 8517a650cfdc control tooltip font via Swing HTML, with tooltip-font-size property; wenzelm parents: 37177 diff changeset	102
38854 eb6a35be18ca Isabelle/jEdit property for global tooltip dismiss delay; wenzelm parents: 38843 diff changeset	103	def tooltip_dismiss_delay(): Int =
eb6a35be18ca Isabelle/jEdit property for global tooltip dismiss delay; wenzelm parents: 38843 diff changeset	104	Int_Property("tooltip-dismiss-delay", 8000) max 500
eb6a35be18ca Isabelle/jEdit property for global tooltip dismiss delay; wenzelm parents: 38843 diff changeset	105
eb6a35be18ca Isabelle/jEdit property for global tooltip dismiss delay; wenzelm parents: 38843 diff changeset	106	def setup_tooltips()
eb6a35be18ca Isabelle/jEdit property for global tooltip dismiss delay; wenzelm parents: 38843 diff changeset	107	{
eb6a35be18ca Isabelle/jEdit property for global tooltip dismiss delay; wenzelm parents: 38843 diff changeset	108	Swing_Thread.now {
eb6a35be18ca Isabelle/jEdit property for global tooltip dismiss delay; wenzelm parents: 38843 diff changeset	109	val manager = javax.swing.ToolTipManager.sharedInstance
eb6a35be18ca Isabelle/jEdit property for global tooltip dismiss delay; wenzelm parents: 38843 diff changeset	110	manager.setDismissDelay(tooltip_dismiss_delay())
eb6a35be18ca Isabelle/jEdit property for global tooltip dismiss delay; wenzelm parents: 38843 diff changeset	111	}
eb6a35be18ca Isabelle/jEdit property for global tooltip dismiss delay; wenzelm parents: 38843 diff changeset	112	}
eb6a35be18ca Isabelle/jEdit property for global tooltip dismiss delay; wenzelm parents: 38843 diff changeset	113
37201 8517a650cfdc control tooltip font via Swing HTML, with tooltip-font-size property; wenzelm parents: 37177 diff changeset	114
39241 e9a442606db3 Isabelle.load_icon with some sanity checks; wenzelm parents: 39167 diff changeset	115	/* icons */
e9a442606db3 Isabelle.load_icon with some sanity checks; wenzelm parents: 39167 diff changeset	116
e9a442606db3 Isabelle.load_icon with some sanity checks; wenzelm parents: 39167 diff changeset	117	def load_icon(name: String): javax.swing.Icon =
e9a442606db3 Isabelle.load_icon with some sanity checks; wenzelm parents: 39167 diff changeset	118	{
e9a442606db3 Isabelle.load_icon with some sanity checks; wenzelm parents: 39167 diff changeset	119	val icon = GUIUtilities.loadIcon(name)
e9a442606db3 Isabelle.load_icon with some sanity checks; wenzelm parents: 39167 diff changeset	120	if (icon.getIconWidth < 0 \|\| icon.getIconHeight < 0)
39630 44181423183a explicit Session.Phase indication with associated event bus; wenzelm parents: 39628 diff changeset	121	Log.log(Log.ERROR, icon, "Bad icon: " + name)
39241 e9a442606db3 Isabelle.load_icon with some sanity checks; wenzelm parents: 39167 diff changeset	122	icon
e9a442606db3 Isabelle.load_icon with some sanity checks; wenzelm parents: 39167 diff changeset	123	}
e9a442606db3 Isabelle.load_icon with some sanity checks; wenzelm parents: 39167 diff changeset	124
e9a442606db3 Isabelle.load_icon with some sanity checks; wenzelm parents: 39167 diff changeset	125
38221 e0f00f0945b4 misc tuning and clarification; wenzelm parents: 37557 diff changeset	126	/* 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	127
37177 17331ca75044 avoid deprecated Iterator.fromArray; wenzelm parents: 37164 diff changeset	128	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	129
37177 17331ca75044 avoid deprecated Iterator.fromArray; wenzelm parents: 37164 diff changeset	130	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	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(view: View): Iterator[JEditTextArea] =
37177 17331ca75044 avoid deprecated Iterator.fromArray; wenzelm parents: 37164 diff changeset	133	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	134
02959dcea756 split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea); wenzelm parents: 34782 diff changeset	135	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	136	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	137
02959dcea756 split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea); wenzelm parents: 34782 diff changeset	138	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	139	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	140
38843 d95522496593 more careful locking of jEdit buffer; wenzelm parents: 38640 diff changeset	141	def buffer_lock[A](buffer: JEditBuffer)(body: => A): A =
38640 105d1f112da5 sporadic locking of jEdit buffer; wenzelm parents: 38222 diff changeset	142	{
105d1f112da5 sporadic locking of jEdit buffer; wenzelm parents: 38222 diff changeset	143	try { buffer.readLock(); body }
105d1f112da5 sporadic locking of jEdit buffer; wenzelm parents: 38222 diff changeset	144	finally { buffer.readUnlock() }
105d1f112da5 sporadic locking of jEdit buffer; wenzelm parents: 38222 diff changeset	145	}
105d1f112da5 sporadic locking of jEdit buffer; wenzelm parents: 38222 diff changeset	146
38843 d95522496593 more careful locking of jEdit buffer; wenzelm parents: 38640 diff changeset	147	def swing_buffer_lock[A](buffer: JEditBuffer)(body: => A): A =
d95522496593 more careful locking of jEdit buffer; wenzelm parents: 38640 diff changeset	148	Swing_Thread.now { buffer_lock(buffer) { body } }
d95522496593 more careful locking of jEdit buffer; wenzelm parents: 38640 diff changeset	149
34784 02959dcea756 split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea); wenzelm parents: 34782 diff changeset	150
37068 07936a4efe93 access statically typed dockable windows; wenzelm parents: 37019 diff changeset	151	/* dockable windows */
07936a4efe93 access statically typed dockable windows; wenzelm parents: 37019 diff changeset	152
07936a4efe93 access statically typed dockable windows; wenzelm parents: 37019 diff changeset	153	private def wm(view: View): DockableWindowManager = view.getDockableWindowManager
07936a4efe93 access statically typed dockable windows; wenzelm parents: 37019 diff changeset	154
39515 57ceabb0bb8e basic setup for prover session panel; wenzelm parents: 39241 diff changeset	155	def docked_session(view: View): Option[Session_Dockable] =
57ceabb0bb8e basic setup for prover session panel; wenzelm parents: 39241 diff changeset	156	wm(view).getDockableWindow("isabelle-session") match {
57ceabb0bb8e basic setup for prover session panel; wenzelm parents: 39241 diff changeset	157	case dockable: Session_Dockable => Some(dockable)
57ceabb0bb8e basic setup for prover session panel; wenzelm parents: 39241 diff changeset	158	case _ => None
57ceabb0bb8e basic setup for prover session panel; wenzelm parents: 39241 diff changeset	159	}
57ceabb0bb8e basic setup for prover session panel; wenzelm parents: 39241 diff changeset	160
37068 07936a4efe93 access statically typed dockable windows; wenzelm parents: 37019 diff changeset	161	def docked_output(view: View): Option[Output_Dockable] =
07936a4efe93 access statically typed dockable windows; wenzelm parents: 37019 diff changeset	162	wm(view).getDockableWindow("isabelle-output") match {
07936a4efe93 access statically typed dockable windows; wenzelm parents: 37019 diff changeset	163	case dockable: Output_Dockable => Some(dockable)
07936a4efe93 access statically typed dockable windows; wenzelm parents: 37019 diff changeset	164	case _ => None
07936a4efe93 access statically typed dockable windows; wenzelm parents: 37019 diff changeset	165	}
07936a4efe93 access statically typed dockable windows; wenzelm parents: 37019 diff changeset	166
07936a4efe93 access statically typed dockable windows; wenzelm parents: 37019 diff changeset	167	def docked_raw_output(view: View): Option[Raw_Output_Dockable] =
07936a4efe93 access statically typed dockable windows; wenzelm parents: 37019 diff changeset	168	wm(view).getDockableWindow("isabelle-raw-output") match {
07936a4efe93 access statically typed dockable windows; wenzelm parents: 37019 diff changeset	169	case dockable: Raw_Output_Dockable => Some(dockable)
07936a4efe93 access statically typed dockable windows; wenzelm parents: 37019 diff changeset	170	case _ => None
07936a4efe93 access statically typed dockable windows; wenzelm parents: 37019 diff changeset	171	}
07936a4efe93 access statically typed dockable windows; wenzelm parents: 37019 diff changeset	172
07936a4efe93 access statically typed dockable windows; wenzelm parents: 37019 diff changeset	173	def docked_protocol(view: View): Option[Protocol_Dockable] =
07936a4efe93 access statically typed dockable windows; wenzelm parents: 37019 diff changeset	174	wm(view).getDockableWindow("isabelle-protocol") match {
07936a4efe93 access statically typed dockable windows; wenzelm parents: 37019 diff changeset	175	case dockable: Protocol_Dockable => Some(dockable)
07936a4efe93 access statically typed dockable windows; wenzelm parents: 37019 diff changeset	176	case _ => None
07936a4efe93 access statically typed dockable windows; wenzelm parents: 37019 diff changeset	177	}
07936a4efe93 access statically typed dockable windows; wenzelm parents: 37019 diff changeset	178
07936a4efe93 access statically typed dockable windows; wenzelm parents: 37019 diff changeset	179
39517 e036c67448e6 separate Isabelle.logic_selector; wenzelm parents: 39515 diff changeset	180	/* logic image */
e036c67448e6 separate Isabelle.logic_selector; wenzelm parents: 39515 diff changeset	181
e036c67448e6 separate Isabelle.logic_selector; wenzelm parents: 39515 diff changeset	182	def default_logic(): String =
e036c67448e6 separate Isabelle.logic_selector; wenzelm parents: 39515 diff changeset	183	{
e036c67448e6 separate Isabelle.logic_selector; wenzelm parents: 39515 diff changeset	184	val logic = system.getenv("JEDIT_LOGIC")
e036c67448e6 separate Isabelle.logic_selector; wenzelm parents: 39515 diff changeset	185	if (logic != "") logic
e036c67448e6 separate Isabelle.logic_selector; wenzelm parents: 39515 diff changeset	186	else system.getenv_strict("ISABELLE_LOGIC")
e036c67448e6 separate Isabelle.logic_selector; wenzelm parents: 39515 diff changeset	187	}
e036c67448e6 separate Isabelle.logic_selector; wenzelm parents: 39515 diff changeset	188
e036c67448e6 separate Isabelle.logic_selector; wenzelm parents: 39515 diff changeset	189	class Logic_Entry(val name: String, val description: String)
e036c67448e6 separate Isabelle.logic_selector; wenzelm parents: 39515 diff changeset	190	{
e036c67448e6 separate Isabelle.logic_selector; wenzelm parents: 39515 diff changeset	191	override def toString = description
e036c67448e6 separate Isabelle.logic_selector; wenzelm parents: 39515 diff changeset	192	}
e036c67448e6 separate Isabelle.logic_selector; wenzelm parents: 39515 diff changeset	193
e036c67448e6 separate Isabelle.logic_selector; wenzelm parents: 39515 diff changeset	194	def logic_selector(logic: String): ComboBox[Logic_Entry] =
e036c67448e6 separate Isabelle.logic_selector; wenzelm parents: 39515 diff changeset	195	{
e036c67448e6 separate Isabelle.logic_selector; wenzelm parents: 39515 diff changeset	196	val entries =
e036c67448e6 separate Isabelle.logic_selector; wenzelm parents: 39515 diff changeset	197	new Logic_Entry("", "default (" + default_logic() + ")") ::
e036c67448e6 separate Isabelle.logic_selector; wenzelm parents: 39515 diff changeset	198	system.find_logics().map(name => new Logic_Entry(name, name))
e036c67448e6 separate Isabelle.logic_selector; wenzelm parents: 39515 diff changeset	199	val component = new ComboBox(entries)
e036c67448e6 separate Isabelle.logic_selector; wenzelm parents: 39515 diff changeset	200	entries.find(_.name == logic) match {
e036c67448e6 separate Isabelle.logic_selector; wenzelm parents: 39515 diff changeset	201	case None =>
e036c67448e6 separate Isabelle.logic_selector; wenzelm parents: 39515 diff changeset	202	case Some(entry) => component.selection.item = entry
e036c67448e6 separate Isabelle.logic_selector; wenzelm parents: 39515 diff changeset	203	}
e036c67448e6 separate Isabelle.logic_selector; wenzelm parents: 39515 diff changeset	204	component
e036c67448e6 separate Isabelle.logic_selector; wenzelm parents: 39515 diff changeset	205	}
34318 c13e168a8ae6 original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout; wenzelm parents: diff changeset	206	}
c13e168a8ae6 original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout; wenzelm parents: diff changeset	207
34429 03afc73e185f tuned; wenzelm parents: 34422 diff changeset	208
34618 e45052ff7233 added Boolean_Property, Int_Property; wenzelm parents: 34615 diff changeset	209	class Plugin extends EBPlugin
e45052ff7233 added Boolean_Property, Int_Property; wenzelm parents: 34615 diff changeset	210	{
39630 44181423183a explicit Session.Phase indication with associated event bus; wenzelm parents: 39628 diff changeset	211	/* session management */
44181423183a explicit Session.Phase indication with associated event bus; wenzelm parents: 39628 diff changeset	212
44181423183a explicit Session.Phase indication with associated event bus; wenzelm parents: 39628 diff changeset	213	private def session_startup()
44181423183a explicit Session.Phase indication with associated event bus; wenzelm parents: 39628 diff changeset	214	{
44181423183a explicit Session.Phase indication with associated event bus; wenzelm parents: 39628 diff changeset	215	val timeout = Isabelle.Int_Property("startup-timeout") max 1000
44181423183a explicit Session.Phase indication with associated event bus; wenzelm parents: 39628 diff changeset	216	val modes = Isabelle.system.getenv("JEDIT_PRINT_MODE").split(",").toList.map("-m" + _)
44181423183a explicit Session.Phase indication with associated event bus; wenzelm parents: 39628 diff changeset	217	val logic = {
44181423183a explicit Session.Phase indication with associated event bus; wenzelm parents: 39628 diff changeset	218	val logic = Isabelle.Property("logic")
44181423183a explicit Session.Phase indication with associated event bus; wenzelm parents: 39628 diff changeset	219	if (logic != null && logic != "") logic
44181423183a explicit Session.Phase indication with associated event bus; wenzelm parents: 39628 diff changeset	220	else Isabelle.default_logic()
44181423183a explicit Session.Phase indication with associated event bus; wenzelm parents: 39628 diff changeset	221	}
44181423183a explicit Session.Phase indication with associated event bus; wenzelm parents: 39628 diff changeset	222	Isabelle.session.start(timeout, modes ::: List(logic))
44181423183a explicit Session.Phase indication with associated event bus; wenzelm parents: 39628 diff changeset	223	}
44181423183a explicit Session.Phase indication with associated event bus; wenzelm parents: 39628 diff changeset	224
44181423183a explicit Session.Phase indication with associated event bus; wenzelm parents: 39628 diff changeset	225	private def activate_buffer(buffer: Buffer)
44181423183a explicit Session.Phase indication with associated event bus; wenzelm parents: 39628 diff changeset	226	{
44181423183a explicit Session.Phase indication with associated event bus; wenzelm parents: 39628 diff changeset	227	Isabelle.swing_buffer_lock(buffer) {
44181423183a explicit Session.Phase indication with associated event bus; wenzelm parents: 39628 diff changeset	228	Thy_Header.split_thy_path(Isabelle.system.posix_path(buffer.getPath)) match {
44181423183a explicit Session.Phase indication with associated event bus; wenzelm parents: 39628 diff changeset	229	case None =>
44181423183a explicit Session.Phase indication with associated event bus; wenzelm parents: 39628 diff changeset	230	case Some((_, thy_name)) =>
44181423183a explicit Session.Phase indication with associated event bus; wenzelm parents: 39628 diff changeset	231	val model = Document_Model.init(Isabelle.session, buffer, thy_name)
44181423183a explicit Session.Phase indication with associated event bus; wenzelm parents: 39628 diff changeset	232	for (text_area <- Isabelle.jedit_text_areas(buffer))
44181423183a explicit Session.Phase indication with associated event bus; wenzelm parents: 39628 diff changeset	233	Document_View.init(model, text_area)
44181423183a explicit Session.Phase indication with associated event bus; wenzelm parents: 39628 diff changeset	234	}
44181423183a explicit Session.Phase indication with associated event bus; wenzelm parents: 39628 diff changeset	235	}
44181423183a explicit Session.Phase indication with associated event bus; wenzelm parents: 39628 diff changeset	236	}
44181423183a explicit Session.Phase indication with associated event bus; wenzelm parents: 39628 diff changeset	237
44181423183a explicit Session.Phase indication with associated event bus; wenzelm parents: 39628 diff changeset	238	private def deactivate_buffer(buffer: Buffer)
44181423183a explicit Session.Phase indication with associated event bus; wenzelm parents: 39628 diff changeset	239	{
44181423183a explicit Session.Phase indication with associated event bus; wenzelm parents: 39628 diff changeset	240	Isabelle.swing_buffer_lock(buffer) {
44181423183a explicit Session.Phase indication with associated event bus; wenzelm parents: 39628 diff changeset	241	for (text_area <- Isabelle.jedit_text_areas(buffer)) {
44181423183a explicit Session.Phase indication with associated event bus; wenzelm parents: 39628 diff changeset	242	if (Document_View(text_area).isDefined) Document_View.exit(text_area)
44181423183a explicit Session.Phase indication with associated event bus; wenzelm parents: 39628 diff changeset	243	}
44181423183a explicit Session.Phase indication with associated event bus; wenzelm parents: 39628 diff changeset	244	if (Document_Model(buffer).isDefined) Document_Model.exit(buffer)
44181423183a explicit Session.Phase indication with associated event bus; wenzelm parents: 39628 diff changeset	245	}
44181423183a explicit Session.Phase indication with associated event bus; wenzelm parents: 39628 diff changeset	246	}
44181423183a explicit Session.Phase indication with associated event bus; wenzelm parents: 39628 diff changeset	247
44181423183a explicit Session.Phase indication with associated event bus; wenzelm parents: 39628 diff changeset	248	private val session_manager = Simple_Thread.actor("session_manager", daemon = true) {
44181423183a explicit Session.Phase indication with associated event bus; wenzelm parents: 39628 diff changeset	249	var finished = false
44181423183a explicit Session.Phase indication with associated event bus; wenzelm parents: 39628 diff changeset	250	while (!finished) {
44181423183a explicit Session.Phase indication with associated event bus; wenzelm parents: 39628 diff changeset	251	receive {
44181423183a explicit Session.Phase indication with associated event bus; wenzelm parents: 39628 diff changeset	252	case (Session.Startup, Session.Exit) =>
44181423183a explicit Session.Phase indication with associated event bus; wenzelm parents: 39628 diff changeset	253	val text = new scala.swing.TextArea(Isabelle.session.syslog())
44181423183a explicit Session.Phase indication with associated event bus; wenzelm parents: 39628 diff changeset	254	text.editable = false
44181423183a explicit Session.Phase indication with associated event bus; wenzelm parents: 39628 diff changeset	255	// FIXME proper view!?
44181423183a explicit Session.Phase indication with associated event bus; wenzelm parents: 39628 diff changeset	256	Library.error_dialog(null, null, "Failed to start Isabelle process", text)
44181423183a explicit Session.Phase indication with associated event bus; wenzelm parents: 39628 diff changeset	257	finished = true
44181423183a explicit Session.Phase indication with associated event bus; wenzelm parents: 39628 diff changeset	258
44181423183a explicit Session.Phase indication with associated event bus; wenzelm parents: 39628 diff changeset	259	case (_, Session.Ready) => Isabelle.jedit_buffers.foreach(activate_buffer)
44181423183a explicit Session.Phase indication with associated event bus; wenzelm parents: 39628 diff changeset	260	case (_, Session.Shutdown) => Isabelle.jedit_buffers.foreach(deactivate_buffer)
44181423183a explicit Session.Phase indication with associated event bus; wenzelm parents: 39628 diff changeset	261	case (_, Session.Terminated) => finished = true
44181423183a explicit Session.Phase indication with associated event bus; wenzelm parents: 39628 diff changeset	262	}
44181423183a explicit Session.Phase indication with associated event bus; wenzelm parents: 39628 diff changeset	263	}
44181423183a explicit Session.Phase indication with associated event bus; wenzelm parents: 39628 diff changeset	264	}
44181423183a explicit Session.Phase indication with associated event bus; wenzelm parents: 39628 diff changeset	265
44181423183a explicit Session.Phase indication with associated event bus; wenzelm parents: 39628 diff changeset	266
34618 e45052ff7233 added Boolean_Property, Int_Property; wenzelm parents: 34615 diff changeset	267	/* main plugin plumbing */
34433 3da749b53842 renamed Plugin.plugin to Plugin.self; wenzelm parents: 34429 diff changeset	268
34767 8dd19c5f8c56 added properties_changed event bus; wenzelm parents: 34764 diff changeset	269	override def handleMessage(message: EBMessage)
34618 e45052ff7233 added Boolean_Property, Int_Property; wenzelm parents: 34615 diff changeset	270	{
34767 8dd19c5f8c56 added properties_changed event bus; wenzelm parents: 34764 diff changeset	271	message match {
39630 44181423183a explicit Session.Phase indication with associated event bus; wenzelm parents: 39628 diff changeset	272	case msg: ViewUpdate
44181423183a explicit Session.Phase indication with associated event bus; wenzelm parents: 39628 diff changeset	273	if msg.getWhat == ViewUpdate.ACTIVATED =>
44181423183a explicit Session.Phase indication with associated event bus; wenzelm parents: 39628 diff changeset	274	session_startup()
44181423183a explicit Session.Phase indication with associated event bus; wenzelm parents: 39628 diff changeset	275
37557 1ae272fd4082 refresh Isabelle token marker after buffer properties changed, e.g. when fold mode is switched; wenzelm parents: 37241 diff changeset	276	case msg: BufferUpdate
1ae272fd4082 refresh Isabelle token marker after buffer properties changed, e.g. when fold mode is switched; wenzelm parents: 37241 diff changeset	277	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	278	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	279	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	280	case _ =>
1ae272fd4082 refresh Isabelle token marker after buffer properties changed, e.g. when fold mode is switched; wenzelm parents: 37241 diff changeset	281	}
1ae272fd4082 refresh Isabelle token marker after buffer properties changed, e.g. when fold mode is switched; wenzelm parents: 37241 diff changeset	282
34767 8dd19c5f8c56 added properties_changed event bus; wenzelm parents: 34764 diff changeset	283	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	284	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	285	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	286	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	287
34787 0feac35069c6 need to handle EditPaneUpdate.CREATED explicitly, not included in EditPaneUpdate.BUFFER_CHANGED; wenzelm parents: 34784 diff changeset	288	def init_view()
0feac35069c6 need to handle EditPaneUpdate.CREATED explicitly, not included in EditPaneUpdate.BUFFER_CHANGED; wenzelm parents: 34784 diff changeset	289	{
34788 3779c54a2d21 direct apply for Document_Model and Document_View; wenzelm parents: 34787 diff changeset	290	Document_Model(buffer) match {
34787 0feac35069c6 need to handle EditPaneUpdate.CREATED explicitly, not included in EditPaneUpdate.BUFFER_CHANGED; wenzelm parents: 34784 diff changeset	291	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	292	case None =>
0feac35069c6 need to handle EditPaneUpdate.CREATED explicitly, not included in EditPaneUpdate.BUFFER_CHANGED; wenzelm parents: 34784 diff changeset	293	}
0feac35069c6 need to handle EditPaneUpdate.CREATED explicitly, not included in EditPaneUpdate.BUFFER_CHANGED; wenzelm parents: 34784 diff changeset	294	}
0feac35069c6 need to handle EditPaneUpdate.CREATED explicitly, not included in EditPaneUpdate.BUFFER_CHANGED; wenzelm parents: 34784 diff changeset	295	def exit_view()
0feac35069c6 need to handle EditPaneUpdate.CREATED explicitly, not included in EditPaneUpdate.BUFFER_CHANGED; wenzelm parents: 34784 diff changeset	296	{
34788 3779c54a2d21 direct apply for Document_Model and Document_View; wenzelm parents: 34787 diff changeset	297	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	298	Document_View.exit(text_area)
0feac35069c6 need to handle EditPaneUpdate.CREATED explicitly, not included in EditPaneUpdate.BUFFER_CHANGED; wenzelm parents: 34784 diff changeset	299	}
34767 8dd19c5f8c56 added properties_changed event bus; wenzelm parents: 34764 diff changeset	300	msg.getWhat match {
34787 0feac35069c6 need to handle EditPaneUpdate.CREATED explicitly, not included in EditPaneUpdate.BUFFER_CHANGED; wenzelm parents: 34784 diff changeset	301	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	302	case EditPaneUpdate.CREATED => init_view()
0feac35069c6 need to handle EditPaneUpdate.CREATED explicitly, not included in EditPaneUpdate.BUFFER_CHANGED; wenzelm parents: 34784 diff changeset	303	case EditPaneUpdate.DESTROYED => exit_view()
34671 d179fcb04cbc output_info specific to prover immler@in.tum.de parents: 34670 diff changeset	304	case _ =>
d179fcb04cbc output_info specific to prover immler@in.tum.de parents: 34670 diff changeset	305	}
34784 02959dcea756 split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea); wenzelm parents: 34782 diff changeset	306
34777 91d6089cef88 class Session models full session, with or without prover process (cf. heaps, browser_info); wenzelm parents: 34774 diff changeset	307	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	308	Swing_Thread.now {
39630 44181423183a explicit Session.Phase indication with associated event bus; wenzelm parents: 39628 diff changeset	309	Isabelle.setup_tooltips()
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	310	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	311	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	312	}
34791 b97d5b38dea4 explicit object Session.Global_Settings; wenzelm parents: 34788 diff changeset	313	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	314
34318 c13e168a8ae6 original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout; wenzelm parents: diff changeset	315	case _ =>
c13e168a8ae6 original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout; wenzelm parents: diff changeset	316	}
c13e168a8ae6 original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout; wenzelm parents: diff changeset	317	}
c13e168a8ae6 original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout; wenzelm parents: diff changeset	318
34618 e45052ff7233 added Boolean_Property, Int_Property; wenzelm parents: 34615 diff changeset	319	override def start()
e45052ff7233 added Boolean_Property, Int_Property; wenzelm parents: 34615 diff changeset	320	{
39630 44181423183a explicit Session.Phase indication with associated event bus; wenzelm parents: 39628 diff changeset	321	Isabelle.setup_tooltips()
34615 5e61055bf35b renamed IsabelleProcess to Isabelle_Process; wenzelm parents: 34612 diff changeset	322	Isabelle.system = new Isabelle_System
34774 1fa466333361 install_fonts; wenzelm parents: 34772 diff changeset	323	Isabelle.system.install_fonts()
39628 f6e82967b5cd Plugin.stop: refrain from invalidating Isabelle.session -- some actors/dockables out there might still refer to it; wenzelm parents: 39518 diff changeset	324	Isabelle.session = new Session(Isabelle.system)
39630 44181423183a explicit Session.Phase indication with associated event bus; wenzelm parents: 39628 diff changeset	325	Isabelle.session.phase_changed += session_manager._2
34318 c13e168a8ae6 original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout; wenzelm parents: diff changeset	326	}
34618 e45052ff7233 added Boolean_Property, Int_Property; wenzelm parents: 34615 diff changeset	327
39628 f6e82967b5cd Plugin.stop: refrain from invalidating Isabelle.session -- some actors/dockables out there might still refer to it; wenzelm parents: 39518 diff changeset	328	override def stop()
34618 e45052ff7233 added Boolean_Property, Int_Property; wenzelm parents: 34615 diff changeset	329	{
39628 f6e82967b5cd Plugin.stop: refrain from invalidating Isabelle.session -- some actors/dockables out there might still refer to it; wenzelm parents: 39518 diff changeset	330	Isabelle.session.stop()
39630 44181423183a explicit Session.Phase indication with associated event bus; wenzelm parents: 39628 diff changeset	331	session_manager._1.join
44181423183a explicit Session.Phase indication with associated event bus; wenzelm parents: 39628 diff changeset	332	Isabelle.session.phase_changed -= session_manager._2
34318 c13e168a8ae6 original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout; wenzelm parents: diff changeset	333	}
c13e168a8ae6 original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout; wenzelm parents: diff changeset	334	}

author	wenzelm
	Thu, 23 Sep 2010 18:44:26 +0200
changeset 39630	44181423183a
parent 39628	f6e82967b5cd
child 39631	cad7a5b7f641
permissions	-rw-r--r--