# HG changeset patch
# User wenzelm
# Date 1442864589 -7200
# Node ID bf194f7c4c8eb2d2745681a4b61c3cbe164d0b7b
# Parent  3e491e34a62e23edc0a865197d5ba751d33d99a4# Parent  1bb5a10b8ce029e20431263ef67a4d1c1bd69451
merged

diff -r 3e491e34a62e -r bf194f7c4c8e NEWS
--- 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.
diff -r 3e491e34a62e -r bf194f7c4c8e etc/options
--- 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)"
 
diff -r 3e491e34a62e -r bf194f7c4c8e lib/Tools/update_then
--- /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
diff -r 3e491e34a62e -r bf194f7c4c8e src/Pure/Isar/isar_syn.ML
--- 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"
diff -r 3e491e34a62e -r bf194f7c4c8e src/Pure/Isar/toplevel.ML
--- 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 ^ ">");
 
diff -r 3e491e34a62e -r bf194f7c4c8e src/Pure/PIDE/command.ML
--- 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);
 
 
diff -r 3e491e34a62e -r bf194f7c4c8e src/Pure/PIDE/markup.ML
--- 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
diff -r 3e491e34a62e -r bf194f7c4c8e src/Pure/PIDE/query_operation.ML
--- 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;
-
diff -r 3e491e34a62e -r bf194f7c4c8e src/Pure/PIDE/query_operation.scala
--- 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 =>
           }
         }
diff -r 3e491e34a62e -r bf194f7c4c8e src/Pure/Tools/print_operation.ML
--- 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;
-
diff -r 3e491e34a62e -r bf194f7c4c8e src/Pure/Tools/update_then.scala
--- /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)))
+    }
+  }
+}
diff -r 3e491e34a62e -r bf194f7c4c8e src/Pure/build-jars
--- 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
diff -r 3e491e34a62e -r bf194f7c4c8e src/Tools/jEdit/lib/Tools/jedit
--- 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"
diff -r 3e491e34a62e -r bf194f7c4c8e src/Tools/jEdit/src/Isabelle.props
--- 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
diff -r 3e491e34a62e -r bf194f7c4c8e src/Tools/jEdit/src/actions.xml
--- 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();
diff -r 3e491e34a62e -r bf194f7c4c8e src/Tools/jEdit/src/dockables.xml
--- 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>
diff -r 3e491e34a62e -r bf194f7c4c8e src/Tools/jEdit/src/isabelle.scala
--- 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
diff -r 3e491e34a62e -r bf194f7c4c8e src/Tools/jEdit/src/jEdit.props
--- 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
diff -r 3e491e34a62e -r bf194f7c4c8e src/Tools/jEdit/src/output_dockable.scala
--- 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)
 }
diff -r 3e491e34a62e -r bf194f7c4c8e src/Tools/jEdit/src/sledgehammer_dockable.scala
--- 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,
diff -r 3e491e34a62e -r bf194f7c4c8e src/Tools/jEdit/src/state_dockable.scala
--- /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()
+  }
+}