--- a/src/Pure/Isar/isar_syn.ML Mon Sep 21 14:56:10 2015 +0200
+++ b/src/Pure/Isar/isar_syn.ML Mon Sep 21 14:56:55 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 14:56:10 2015 +0200
+++ b/src/Pure/Isar/toplevel.ML Mon Sep 21 14:56:55 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 14:56:10 2015 +0200
+++ b/src/Pure/PIDE/command.ML Mon Sep 21 14:56:55 2015 +0200
@@ -359,7 +359,9 @@
(fn {keywords, command_name, ...} =>
if 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/query_operation.ML Mon Sep 21 14:56:10 2015 +0200
+++ b/src/Pure/PIDE/query_operation.ML Mon Sep 21 14:56:55 2015 +0200
@@ -17,23 +17,33 @@
fun register {name, pri} f =
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.writelnN, []) s);
+ fun toplevel_error exn =
+ result (Markup.markup (Markup.errorN, []) (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 + 2}
+ (fn {state = st, output_result, ...} =>
+ if Toplevel.is_proof st
+ then output_result (Markup.markup (Markup.stateN, []) (Toplevel.string_of_state st))
+ else ());
end;
--- a/src/Tools/jEdit/lib/Tools/jedit Mon Sep 21 14:56:10 2015 +0200
+++ b/src/Tools/jEdit/lib/Tools/jedit Mon Sep 21 14:56:55 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 14:56:10 2015 +0200
+++ b/src/Tools/jEdit/src/Isabelle.props Mon Sep 21 14:56:55 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/dockables.xml Mon Sep 21 14:56:10 2015 +0200
+++ b/src/Tools/jEdit/src/dockables.xml Mon Sep 21 14:56:55 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 14:56:10 2015 +0200
+++ b/src/Tools/jEdit/src/isabelle.scala Mon Sep 21 14:56:55 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)
--- a/src/Tools/jEdit/src/jEdit.props Mon Sep 21 14:56:10 2015 +0200
+++ b/src/Tools/jEdit/src/jEdit.props Mon Sep 21 14:56:55 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
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/jEdit/src/state_dockable.scala Mon Sep 21 14:56:55 2015 +0200
@@ -0,0 +1,101 @@
+/* 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))
+ }
+
+
+ /* controls */
+
+ private val update = new Button("Update") {
+ tooltip = "Update display according to the command at cursor position"
+ reactions += { case ButtonClicked(_) => print_state.apply_query(Nil) }
+ }
+
+ private val locate = 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, locate,
+ pretty_text_area.search_label, pretty_text_area.search_field, zoom)
+ add(controls.peer, BorderLayout.NORTH)
+
+ override def focusOnDefaultComponent { update.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()
+ }
+}