--- a/NEWS Mon Sep 21 19:52:13 2015 +0100
+++ b/NEWS Mon Sep 21 21:43:09 2015 +0200
@@ -28,6 +28,12 @@
asynchronously, leading to much better editor reactivity. Moreover, the
full document node content is taken into account.
+* The State panel manages explicit proof state output, with jEdit action
+"isabelle.update-state" (shortcut S+ENTER) to trigger update according
+to cursor position. Option "editor_output_state" controls implicit proof
+state output in the Output panel: suppressing this reduces resource
+requirements of prover time and GUI space.
+
*** Isar ***
@@ -362,6 +368,15 @@
running Isabelle/jEdit process. This achieves the effect of
single-instance applications seen on common GUI desktops.
+* Command-line tool "isabelle update_then" expands old Isar command
+conflations:
+
+ hence ~> then have
+ thus ~> then show
+
+This syntax is more orthogonal and improves readability and
+maintainability of proofs.
+
* Poly/ML default platform architecture may be changed from 32bit to
64bit via system option ML_system_64. A system restart (and rebuild)
is required after change.
--- a/etc/options Mon Sep 21 19:52:13 2015 +0100
+++ b/etc/options Mon Sep 21 21:43:09 2015 +0200
@@ -140,6 +140,9 @@
public option editor_continuous_checking : bool = true
-- "continuous checking of proof document (visible and required parts)"
+public option editor_output_state : bool = true
+ -- "implicit output of proof state"
+
option editor_execution_delay : real = 0.02
-- "delay for start of execution process after document update (seconds)"
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/lib/Tools/update_then Mon Sep 21 21:43:09 2015 +0200
@@ -0,0 +1,38 @@
+#!/usr/bin/env bash
+#
+# Author: Makarius
+#
+# DESCRIPTION: expand old Isar command conflations 'hence' and 'thus'
+
+
+## diagnostics
+
+PRG="$(basename "$0")"
+
+function usage()
+{
+ echo
+ echo "Usage: isabelle $PRG [FILES|DIRS...]"
+ echo
+ echo " Recursively find .thy files and expand old Isar command conflations:"
+ echo
+ echo " hence ~> then have"
+ echo " thus ~> then show"
+ echo
+ echo " Old versions of files are preserved by appending \"~~\"."
+ echo
+ exit 1
+}
+
+
+## process command line
+
+[ "$#" -eq 0 -o "$1" = "-?" ] && usage
+
+SPECS="$@"; shift "$#"
+
+
+## main
+
+find $SPECS -name \*.thy -print0 | \
+ xargs -0 "$ISABELLE_TOOL" java isabelle.Update_Then
--- a/src/Pure/Isar/isar_syn.ML Mon Sep 21 19:52:13 2015 +0100
+++ b/src/Pure/Isar/isar_syn.ML Mon Sep 21 21:43:09 2015 +0200
@@ -914,7 +914,8 @@
val _ =
Outer_Syntax.command @{command_keyword print_state}
"print current proof state (if present)"
- (opt_modes >> (fn modes => Toplevel.keep (Print_Mode.with_modes modes Toplevel.print_state)));
+ (opt_modes >> (fn modes =>
+ Toplevel.keep (Print_Mode.with_modes modes (Output.state o Toplevel.string_of_state))));
val _ =
Outer_Syntax.command @{command_keyword welcome} "print welcome message"
--- a/src/Pure/Isar/toplevel.ML Mon Sep 21 19:52:13 2015 +0100
+++ b/src/Pure/Isar/toplevel.ML Mon Sep 21 21:43:09 2015 +0200
@@ -24,7 +24,7 @@
val end_theory: Position.T -> state -> theory
val pretty_context: state -> Pretty.T list
val pretty_state: state -> Pretty.T list
- val print_state: state -> unit
+ val string_of_state: state -> string
val pretty_abstract: state -> Pretty.T
val profiling: int Unsynchronized.ref
type transition
@@ -196,7 +196,7 @@
| SOME (Proof (prf, _)) => Proof.pretty_state (Proof_Node.current prf)
| SOME (Skipped_Proof (d, _)) => [Pretty.str ("skipped proof: depth " ^ string_of_int d)]);
-val print_state = pretty_state #> Pretty.chunks #> Pretty.string_of #> Output.state;
+val string_of_state = pretty_state #> Pretty.chunks #> Pretty.string_of;
fun pretty_abstract state = Pretty.str ("<Isar " ^ str_of_state state ^ ">");
--- a/src/Pure/PIDE/command.ML Mon Sep 21 19:52:13 2015 +0100
+++ b/src/Pure/PIDE/command.ML Mon Sep 21 21:43:09 2015 +0200
@@ -357,9 +357,12 @@
val _ =
print_function "print_state"
(fn {keywords, command_name, ...} =>
- if Keyword.is_printed keywords command_name then
+ if Options.default_bool "editor_output_state" andalso Keyword.is_printed keywords command_name
+ then
SOME {delay = NONE, pri = Task_Queue.urgent_pri + 1, persistent = false, strict = false,
- print_fn = fn _ => fn st => if Toplevel.is_proof st then Toplevel.print_state st else ()}
+ print_fn = fn _ => fn st =>
+ if Toplevel.is_proof st then Output.state (Toplevel.string_of_state st)
+ else ()}
else NONE);
--- a/src/Pure/PIDE/markup.ML Mon Sep 21 19:52:13 2015 +0100
+++ b/src/Pure/PIDE/markup.ML Mon Sep 21 21:43:09 2015 +0200
@@ -155,16 +155,16 @@
val failedN: string val failed: T
val exec_idN: string
val initN: string
- val statusN: string
- val resultN: string
- val writelnN: string
- val stateN: string
- val informationN: string
- val tracingN: string
- val warningN: string
- val legacyN: string
- val errorN: string
- val systemN: string
+ val statusN: string val status: T
+ val resultN: string val result: T
+ val writelnN: string val writeln: T
+ val stateN: string val state: T
+ val informationN: string val information: T
+ val tracingN: string val tracing: T
+ val warningN: string val warning: T
+ val legacyN: string val legacy: T
+ val errorN: string val error: T
+ val systemN: string val system: T
val protocolN: string
val reportN: string val report: T
val no_reportN: string val no_report: T
@@ -550,16 +550,16 @@
val exec_idN = "exec_id";
val initN = "init";
-val statusN = "status";
-val resultN = "result";
-val writelnN = "writeln";
-val stateN = "state"
-val informationN = "information";
-val tracingN = "tracing";
-val warningN = "warning";
-val legacyN = "legacy";
-val errorN = "error";
-val systemN = "system";
+val (statusN, status) = markup_elem "status";
+val (resultN, result) = markup_elem "result";
+val (writelnN, writeln) = markup_elem "writeln";
+val (stateN, state) = markup_elem "state"
+val (informationN, information) = markup_elem "information";
+val (tracingN, tracing) = markup_elem "tracing";
+val (warningN, warning) = markup_elem "warning";
+val (legacyN, legacy) = markup_elem "legacy";
+val (errorN, error) = markup_elem "error";
+val (systemN, system) = markup_elem "system";
val protocolN = "protocol";
val (reportN, report) = markup_elem "report";
@@ -645,7 +645,7 @@
fun add_mode name output =
Synchronized.change modes (fn tab =>
(if not (Symtab.defined tab name) then ()
- else warning ("Redefining markup mode " ^ quote name);
+ else Output.warning ("Redefining markup mode " ^ quote name);
Symtab.update (name, {output = output}) tab));
fun get_mode () =
the_default default
--- a/src/Pure/PIDE/query_operation.ML Mon Sep 21 19:52:13 2015 +0100
+++ b/src/Pure/PIDE/query_operation.ML Mon Sep 21 21:43:09 2015 +0200
@@ -15,26 +15,34 @@
struct
fun register {name, pri} f =
- Command.print_function name
+ Command.print_function (name ^ "_query")
(fn {args = instance :: args, ...} =>
- SOME {delay = NONE, pri = pri, persistent = false, strict = false,
- print_fn = fn _ => uninterruptible (fn restore_attributes => fn state =>
- let
- fun result s = Output.result [(Markup.instanceN, instance)] [s];
- fun status m = result (Markup.markup_only m);
- fun output_result s = result (Markup.markup (Markup.writelnN, []) s);
- fun toplevel_error exn =
- result (Markup.markup (Markup.errorN, []) (Runtime.exn_message exn));
+ SOME {delay = NONE, pri = pri, persistent = false, strict = false,
+ print_fn = fn _ => uninterruptible (fn restore_attributes => fn state =>
+ let
+ fun result s = Output.result [(Markup.instanceN, instance)] [s];
+ fun status m = result (Markup.markup_only m);
+ fun output_result s = result (Markup.markup Markup.writeln s);
+ fun toplevel_error exn = result (Markup.markup Markup.error (Runtime.exn_message exn));
- val _ = status Markup.running;
- fun run () = f {state = state, args = args, output_result = output_result};
- val _ =
- (case Exn.capture (*sic!*) (restore_attributes run) () of
- Exn.Res () => ()
- | Exn.Exn exn => toplevel_error exn);
- val _ = status Markup.finished;
- in () end)}
- | _ => NONE);
+ val _ = status Markup.running;
+ fun run () = f {state = state, args = args, output_result = output_result};
+ val _ =
+ (case Exn.capture (*sic!*) (restore_attributes run) () of
+ Exn.Res () => ()
+ | Exn.Exn exn => toplevel_error exn);
+ val _ = status Markup.finished;
+ in () end)}
+ | _ => NONE);
+
+
+(* print_state *)
+
+val _ =
+ register {name = "print_state", pri = Task_Queue.urgent_pri}
+ (fn {state = st, output_result, ...} =>
+ if Toplevel.is_proof st
+ then output_result (Markup.markup Markup.state (Toplevel.string_of_state st))
+ else ());
end;
-
--- a/src/Pure/PIDE/query_operation.scala Mon Sep 21 19:52:13 2015 +0100
+++ b/src/Pure/PIDE/query_operation.scala Mon Sep 21 21:43:09 2015 +0200
@@ -25,6 +25,7 @@
consume_status: Query_Operation.Status.Value => Unit,
consume_output: (Document.Snapshot, Command.Results, XML.Body) => Unit)
{
+ private val print_function = operation_name + "_query"
private val instance = Document_ID.make().toString
@@ -37,6 +38,8 @@
@volatile private var current_status = Query_Operation.Status.FINISHED
@volatile private var current_exec_id = Document_ID.none
+ def get_location: Option[Command] = current_location
+
private def reset_state()
{
current_location = None
@@ -52,7 +55,7 @@
current_location match {
case None =>
case Some(command) =>
- editor.remove_overlay(command, operation_name, instance :: current_query)
+ editor.remove_overlay(command, print_function, instance :: current_query)
editor.flush()
}
}
@@ -184,7 +187,7 @@
current_location = Some(command)
current_query = query
current_status = Query_Operation.Status.WAITING
- editor.insert_overlay(command, operation_name, instance :: query)
+ editor.insert_overlay(command, print_function, instance :: query)
case None =>
}
}
--- a/src/Pure/Tools/print_operation.ML Mon Sep 21 19:52:13 2015 +0100
+++ b/src/Pure/Tools/print_operation.ML Mon Sep 21 21:43:09 2015 +0200
@@ -76,8 +76,4 @@
register "theorems" "theorems of local theory or proof context"
(Isar_Cmd.pretty_theorems false);
-val _ =
- register "state" "proof state" Toplevel.pretty_state;
-
end;
-
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/Tools/update_then.scala Mon Sep 21 21:43:09 2015 +0200
@@ -0,0 +1,39 @@
+/* Title: Pure/Tools/update_then.scala
+ Author: Makarius
+
+Expand old Isar command conflations 'hence' and 'thus'.
+*/
+
+package isabelle
+
+
+object Update_Then
+{
+ def update_then(path: Path)
+ {
+ val text0 = File.read(path)
+ val text1 =
+ (for (tok <- Token.explode(Keyword.Keywords.empty, text0).iterator)
+ yield {
+ tok.source match {
+ case "hence" => "then have"
+ case "thus" => "then show"
+ case s => s
+ } }).mkString
+
+ if (text0 != text1) {
+ Output.writeln("changing " + path)
+ File.write_backup2(path, text1)
+ }
+ }
+
+
+ /* command line entry point */
+
+ def main(args: Array[String])
+ {
+ Command_Line.tool0 {
+ args.foreach(arg => update_then(Path.explode(arg)))
+ }
+ }
+}
--- a/src/Pure/build-jars Mon Sep 21 19:52:13 2015 +0100
+++ b/src/Pure/build-jars Mon Sep 21 21:43:09 2015 +0200
@@ -105,6 +105,7 @@
Tools/update_cartouches.scala
Tools/update_header.scala
Tools/update_semicolons.scala
+ Tools/update_then.scala
library.scala
term.scala
term_xml.scala
--- a/src/Tools/jEdit/lib/Tools/jedit Mon Sep 21 19:52:13 2015 +0100
+++ b/src/Tools/jEdit/lib/Tools/jedit Mon Sep 21 21:43:09 2015 +0200
@@ -59,6 +59,7 @@
"src/simplifier_trace_window.scala"
"src/sledgehammer_dockable.scala"
"src/spell_checker.scala"
+ "src/state_dockable.scala"
"src/structure_matching.scala"
"src/symbols_dockable.scala"
"src/syslog_dockable.scala"
--- a/src/Tools/jEdit/src/Isabelle.props Mon Sep 21 19:52:13 2015 +0100
+++ b/src/Tools/jEdit/src/Isabelle.props Mon Sep 21 21:43:09 2015 +0200
@@ -39,6 +39,7 @@
isabelle-raw-output \
isabelle-simplifier-trace \
isabelle-sledgehammer \
+ isabelle-state \
isabelle-symbols \
isabelle-syslog \
isabelle-theories \
@@ -65,6 +66,8 @@
isabelle-simplifier-trace.title=Simplifier Trace
isabelle-sledgehammer.label=Sledgehammer panel
isabelle-sledgehammer.title=Sledgehammer
+isabelle-state.label=State panel
+isabelle-state.title=State
isabelle-symbols.label=Symbols panel
isabelle-symbols.title=Symbols
isabelle-syslog.label=Syslog panel
--- a/src/Tools/jEdit/src/actions.xml Mon Sep 21 19:52:13 2015 +0100
+++ b/src/Tools/jEdit/src/actions.xml Mon Sep 21 21:43:09 2015 +0200
@@ -32,6 +32,11 @@
isabelle.jedit.Isabelle.toggle_node_required(view);
</CODE>
</ACTION>
+ <ACTION NAME="isabelle.update-state">
+ <CODE>
+ isabelle.jedit.Isabelle.update_state(view);
+ </CODE>
+ </ACTION>
<ACTION NAME="isabelle.reset-font-size">
<CODE>
isabelle.jedit.Isabelle.reset_font_size();
--- a/src/Tools/jEdit/src/dockables.xml Mon Sep 21 19:52:13 2015 +0100
+++ b/src/Tools/jEdit/src/dockables.xml Mon Sep 21 21:43:09 2015 +0200
@@ -35,6 +35,9 @@
<DOCKABLE NAME="isabelle-sledgehammer" MOVABLE="TRUE">
new isabelle.jedit.Sledgehammer_Dockable(view, position);
</DOCKABLE>
+ <DOCKABLE NAME="isabelle-state" MOVABLE="TRUE">
+ new isabelle.jedit.State_Dockable(view, position);
+ </DOCKABLE>
<DOCKABLE NAME="isabelle-symbols" MOVABLE="TRUE">
new isabelle.jedit.Symbols_Dockable(view, position);
</DOCKABLE>
--- a/src/Tools/jEdit/src/isabelle.scala Mon Sep 21 19:52:13 2015 +0100
+++ b/src/Tools/jEdit/src/isabelle.scala Mon Sep 21 21:43:09 2015 +0200
@@ -147,6 +147,12 @@
case _ => None
}
+ def state_dockable(view: View): Option[State_Dockable] =
+ wm(view).getDockableWindow("isabelle-state") match {
+ case dockable: State_Dockable => Some(dockable)
+ case _ => None
+ }
+
def symbols_dockable(view: View): Option[Symbols_Dockable] =
wm(view).getDockableWindow("isabelle-symbols") match {
case dockable: Symbols_Dockable => Some(dockable)
@@ -199,6 +205,12 @@
}
+ /* update state */
+
+ def update_state(view: View): Unit =
+ state_dockable(view).foreach(_.update())
+
+
/* ML statistics */
class ML_Stats extends
--- a/src/Tools/jEdit/src/jEdit.props Mon Sep 21 19:52:13 2015 +0100
+++ b/src/Tools/jEdit/src/jEdit.props Mon Sep 21 21:43:09 2015 +0200
@@ -193,6 +193,7 @@
isabelle-query.dock-position=bottom
isabelle-simplifier-trace.dock-position=floating
isabelle-sledgehammer.dock-position=bottom
+isabelle-state.dock-position=right
isabelle-symbols.dock-position=bottom
isabelle-theories.dock-position=right
isabelle.complete-word.label=Complete word
@@ -231,6 +232,8 @@
isabelle.toggle-continuous-checking.shortcut=C+e ENTER
isabelle.toggle-node-required.label=Toggle node required
isabelle.toggle-node-required.shortcut=C+e SPACE
+isabelle.update-state.label=Update state output
+isabelle.update-state.shortcut=S+ENTER
lang.usedefaultlocale=false
largefilemode=full
line-end.shortcut=END
--- a/src/Tools/jEdit/src/output_dockable.scala Mon Sep 21 19:52:13 2015 +0100
+++ b/src/Tools/jEdit/src/output_dockable.scala Mon Sep 21 21:43:09 2015 +0200
@@ -37,8 +37,6 @@
override def detach_operation = pretty_text_area.detach_operation
- private val zoom = new Font_Info.Zoom_Box { def changed = handle_resize() }
-
private def handle_resize()
{
GUI_Thread.require {}
@@ -83,6 +81,28 @@
}
+ /* controls */
+
+ private val auto_update = new CheckBox("Auto update") {
+ tooltip = "Indicate automatic update following cursor movement"
+ reactions += {
+ case ButtonClicked(_) => do_update = this.selected; handle_update(do_update, None) }
+ selected = do_update
+ }
+
+ private val update = new Button("Update") {
+ tooltip = "Update display according to the command at cursor position"
+ reactions += { case ButtonClicked(_) => handle_update(true, None) }
+ }
+
+ private val zoom = new Font_Info.Zoom_Box { def changed = handle_resize() }
+
+ private val controls =
+ new Wrap_Panel(Wrap_Panel.Alignment.Right)(auto_update, update,
+ pretty_text_area.search_label, pretty_text_area.search_field, zoom)
+ add(controls.peer, BorderLayout.NORTH)
+
+
/* main */
private val main =
@@ -124,24 +144,4 @@
override def componentResized(e: ComponentEvent) { delay_resize.invoke() }
override def componentShown(e: ComponentEvent) { delay_resize.invoke() }
})
-
-
- /* controls */
-
- private val auto_update = new CheckBox("Auto update") {
- tooltip = "Indicate automatic update following cursor movement"
- reactions += {
- case ButtonClicked(_) => do_update = this.selected; handle_update(do_update, None) }
- selected = do_update
- }
-
- private val update = new Button("Update") {
- tooltip = "Update display according to the command at cursor position"
- reactions += { case ButtonClicked(_) => handle_update(true, None) }
- }
-
- private val controls =
- new Wrap_Panel(Wrap_Panel.Alignment.Right)(auto_update, update,
- pretty_text_area.search_label, pretty_text_area.search_field, zoom)
- add(controls.peer, BorderLayout.NORTH)
}
--- a/src/Tools/jEdit/src/sledgehammer_dockable.scala Mon Sep 21 19:52:13 2015 +0100
+++ b/src/Tools/jEdit/src/sledgehammer_dockable.scala Mon Sep 21 21:43:09 2015 +0200
@@ -21,6 +21,11 @@
class Sledgehammer_Dockable(view: View, position: String) extends Dockable(view, position)
{
+ GUI_Thread.require {}
+
+
+ /* text area */
+
val pretty_text_area = new Pretty_Text_Area(view)
set_content(pretty_text_area)
@@ -51,7 +56,13 @@
/* resize */
- private val zoom = new Font_Info.Zoom_Box { def changed = handle_resize() }
+ private val delay_resize =
+ GUI_Thread.delay_first(PIDE.options.seconds("editor_update_delay")) { handle_resize() }
+
+ addComponentListener(new ComponentAdapter {
+ override def componentResized(e: ComponentEvent) { delay_resize.invoke() }
+ override def componentShown(e: ComponentEvent) { delay_resize.invoke() }
+ })
private def handle_resize()
{
@@ -61,14 +72,6 @@
Font_Info.main(PIDE.options.real("jedit_font_scale") * zoom.factor / 100))
}
- private val delay_resize =
- GUI_Thread.delay_first(PIDE.options.seconds("editor_update_delay")) { handle_resize() }
-
- addComponentListener(new ComponentAdapter {
- override def componentResized(e: ComponentEvent) { delay_resize.invoke() }
- override def componentShown(e: ComponentEvent) { delay_resize.invoke() }
- })
-
/* controls */
@@ -131,6 +134,8 @@
reactions += { case ButtonClicked(_) => sledgehammer.locate_query() }
}
+ private val zoom = new Font_Info.Zoom_Box { def changed = handle_resize() }
+
private val controls =
new Wrap_Panel(Wrap_Panel.Alignment.Right)(
provers_label, Component.wrap(provers), isar_proofs, try0,
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/jEdit/src/state_dockable.scala Mon Sep 21 21:43:09 2015 +0200
@@ -0,0 +1,118 @@
+/* Title: Tools/jEdit/src/state_dockable.scala
+ Author: Makarius
+
+Dockable window for proof state output.
+*/
+
+package isabelle.jedit
+
+
+import isabelle._
+
+import scala.swing.{Button, CheckBox}
+import scala.swing.event.ButtonClicked
+
+import java.awt.BorderLayout
+import java.awt.event.{ComponentEvent, ComponentAdapter}
+
+import org.gjt.sp.jedit.View
+
+
+class State_Dockable(view: View, position: String) extends Dockable(view, position)
+{
+ GUI_Thread.require {}
+
+
+ /* text area */
+
+ val pretty_text_area = new Pretty_Text_Area(view)
+ set_content(pretty_text_area)
+
+ override def detach_operation = pretty_text_area.detach_operation
+
+ private val print_state =
+ new Query_Operation(PIDE.editor, view, "print_state", _ => (),
+ (snapshot, results, body) =>
+ pretty_text_area.update(snapshot, results, Pretty.separate(body)))
+
+
+ /* resize */
+
+ private val delay_resize =
+ GUI_Thread.delay_first(PIDE.options.seconds("editor_update_delay")) { handle_resize() }
+
+ addComponentListener(new ComponentAdapter {
+ override def componentResized(e: ComponentEvent) { delay_resize.invoke() }
+ override def componentShown(e: ComponentEvent) { delay_resize.invoke() }
+ })
+
+ private def handle_resize()
+ {
+ GUI_Thread.require {}
+
+ pretty_text_area.resize(
+ Font_Info.main(PIDE.options.real("jedit_font_scale") * zoom.factor / 100))
+ }
+
+
+ /* update */
+
+ def update()
+ {
+ GUI_Thread.require {}
+
+ PIDE.document_model(view.getBuffer).map(_.snapshot()) match {
+ case Some(snapshot) =>
+ (PIDE.editor.current_command(view, snapshot), print_state.get_location) match {
+ case (Some(command1), Some(command2)) if command1.id == command2.id =>
+ case _ => print_state.apply_query(Nil)
+ }
+ case None =>
+ }
+ }
+
+
+ /* controls */
+
+ private val update_button = new Button("<html><b>Update</b></html>") {
+ tooltip = "Update display according to the command at cursor position"
+ reactions += { case ButtonClicked(_) => print_state.apply_query(Nil) }
+ }
+
+ private val locate_button = new Button("Locate") {
+ tooltip = "Locate printed command within source text"
+ reactions += { case ButtonClicked(_) => print_state.locate_query() }
+ }
+
+ private val zoom = new Font_Info.Zoom_Box { def changed = handle_resize() }
+
+ private val controls =
+ new Wrap_Panel(Wrap_Panel.Alignment.Right)(update_button, locate_button,
+ pretty_text_area.search_label, pretty_text_area.search_field, zoom)
+ add(controls.peer, BorderLayout.NORTH)
+
+ override def focusOnDefaultComponent { update_button.requestFocus }
+
+
+ /* main */
+
+ private val main =
+ Session.Consumer[Any](getClass.getName) {
+ case _: Session.Global_Options =>
+ GUI_Thread.later { handle_resize() }
+ }
+
+ override def init()
+ {
+ PIDE.session.global_options += main
+ handle_resize()
+ print_state.activate()
+ }
+
+ override def exit()
+ {
+ print_state.deactivate()
+ PIDE.session.global_options -= main
+ delay_resize.revoke()
+ }
+}