# HG changeset patch # User wenzelm # Date 1442840215 -7200 # Node ID 19118f9b939d309640859321b231644211ba9945 # Parent 46fa8f71e0edc852bba363370ef8aea80fe32086 separate panel for proof state output; diff -r 46fa8f71e0ed -r 19118f9b939d src/Pure/Isar/isar_syn.ML --- 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" diff -r 46fa8f71e0ed -r 19118f9b939d src/Pure/Isar/toplevel.ML --- 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 (""); diff -r 46fa8f71e0ed -r 19118f9b939d src/Pure/PIDE/command.ML --- 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); diff -r 46fa8f71e0ed -r 19118f9b939d src/Pure/PIDE/query_operation.ML --- 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; diff -r 46fa8f71e0ed -r 19118f9b939d src/Tools/jEdit/lib/Tools/jedit --- 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" diff -r 46fa8f71e0ed -r 19118f9b939d src/Tools/jEdit/src/Isabelle.props --- 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 diff -r 46fa8f71e0ed -r 19118f9b939d src/Tools/jEdit/src/dockables.xml --- 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 @@ new isabelle.jedit.Sledgehammer_Dockable(view, position); + + new isabelle.jedit.State_Dockable(view, position); + new isabelle.jedit.Symbols_Dockable(view, position); diff -r 46fa8f71e0ed -r 19118f9b939d src/Tools/jEdit/src/isabelle.scala --- 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) diff -r 46fa8f71e0ed -r 19118f9b939d src/Tools/jEdit/src/jEdit.props --- 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 diff -r 46fa8f71e0ed -r 19118f9b939d 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 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() + } +}