separate panel for proof state output;
authorwenzelm
Mon Sep 21 14:56:55 2015 +0200 (2015-09-21 ago)
changeset 6120819118f9b939d
parent 61207 46fa8f71e0ed
child 61209 7a421e7ef97c
separate panel for proof state output;
src/Pure/Isar/isar_syn.ML
src/Pure/Isar/toplevel.ML
src/Pure/PIDE/command.ML
src/Pure/PIDE/query_operation.ML
src/Tools/jEdit/lib/Tools/jedit
src/Tools/jEdit/src/Isabelle.props
src/Tools/jEdit/src/dockables.xml
src/Tools/jEdit/src/isabelle.scala
src/Tools/jEdit/src/jEdit.props
src/Tools/jEdit/src/state_dockable.scala
     1.1 --- a/src/Pure/Isar/isar_syn.ML	Mon Sep 21 14:56:10 2015 +0200
     1.2 +++ b/src/Pure/Isar/isar_syn.ML	Mon Sep 21 14:56:55 2015 +0200
     1.3 @@ -914,7 +914,8 @@
     1.4  val _ =
     1.5    Outer_Syntax.command @{command_keyword print_state}
     1.6      "print current proof state (if present)"
     1.7 -    (opt_modes >> (fn modes => Toplevel.keep (Print_Mode.with_modes modes Toplevel.print_state)));
     1.8 +    (opt_modes >> (fn modes =>
     1.9 +      Toplevel.keep (Print_Mode.with_modes modes (Output.state o Toplevel.string_of_state))));
    1.10  
    1.11  val _ =
    1.12    Outer_Syntax.command @{command_keyword welcome} "print welcome message"
     2.1 --- a/src/Pure/Isar/toplevel.ML	Mon Sep 21 14:56:10 2015 +0200
     2.2 +++ b/src/Pure/Isar/toplevel.ML	Mon Sep 21 14:56:55 2015 +0200
     2.3 @@ -24,7 +24,7 @@
     2.4    val end_theory: Position.T -> state -> theory
     2.5    val pretty_context: state -> Pretty.T list
     2.6    val pretty_state: state -> Pretty.T list
     2.7 -  val print_state: state -> unit
     2.8 +  val string_of_state: state -> string
     2.9    val pretty_abstract: state -> Pretty.T
    2.10    val profiling: int Unsynchronized.ref
    2.11    type transition
    2.12 @@ -196,7 +196,7 @@
    2.13    | SOME (Proof (prf, _)) => Proof.pretty_state (Proof_Node.current prf)
    2.14    | SOME (Skipped_Proof (d, _)) => [Pretty.str ("skipped proof: depth " ^ string_of_int d)]);
    2.15  
    2.16 -val print_state = pretty_state #> Pretty.chunks #> Pretty.string_of #> Output.state;
    2.17 +val string_of_state = pretty_state #> Pretty.chunks #> Pretty.string_of;
    2.18  
    2.19  fun pretty_abstract state = Pretty.str ("<Isar " ^ str_of_state state ^ ">");
    2.20  
     3.1 --- a/src/Pure/PIDE/command.ML	Mon Sep 21 14:56:10 2015 +0200
     3.2 +++ b/src/Pure/PIDE/command.ML	Mon Sep 21 14:56:55 2015 +0200
     3.3 @@ -359,7 +359,9 @@
     3.4      (fn {keywords, command_name, ...} =>
     3.5        if Keyword.is_printed keywords command_name then
     3.6          SOME {delay = NONE, pri = Task_Queue.urgent_pri + 1, persistent = false, strict = false,
     3.7 -          print_fn = fn _ => fn st => if Toplevel.is_proof st then Toplevel.print_state st else ()}
     3.8 +          print_fn = fn _ => fn st =>
     3.9 +            if Toplevel.is_proof st then Output.state (Toplevel.string_of_state st)
    3.10 +            else ()}
    3.11        else NONE);
    3.12  
    3.13  
     4.1 --- a/src/Pure/PIDE/query_operation.ML	Mon Sep 21 14:56:10 2015 +0200
     4.2 +++ b/src/Pure/PIDE/query_operation.ML	Mon Sep 21 14:56:55 2015 +0200
     4.3 @@ -17,23 +17,33 @@
     4.4  fun register {name, pri} f =
     4.5    Command.print_function (name ^ "_query")
     4.6      (fn {args = instance :: args, ...} =>
     4.7 -        SOME {delay = NONE, pri = pri, persistent = false, strict = false,
     4.8 -          print_fn = fn _ => uninterruptible (fn restore_attributes => fn state =>
     4.9 -            let
    4.10 -              fun result s = Output.result [(Markup.instanceN, instance)] [s];
    4.11 -              fun status m = result (Markup.markup_only m);
    4.12 -              fun output_result s = result (Markup.markup (Markup.writelnN, []) s);
    4.13 -              fun toplevel_error exn =
    4.14 -                result (Markup.markup (Markup.errorN, []) (Runtime.exn_message exn));
    4.15 +      SOME {delay = NONE, pri = pri, persistent = false, strict = false,
    4.16 +        print_fn = fn _ => uninterruptible (fn restore_attributes => fn state =>
    4.17 +          let
    4.18 +            fun result s = Output.result [(Markup.instanceN, instance)] [s];
    4.19 +            fun status m = result (Markup.markup_only m);
    4.20 +            fun output_result s = result (Markup.markup (Markup.writelnN, []) s);
    4.21 +            fun toplevel_error exn =
    4.22 +              result (Markup.markup (Markup.errorN, []) (Runtime.exn_message exn));
    4.23  
    4.24 -              val _ = status Markup.running;
    4.25 -              fun run () = f {state = state, args = args, output_result = output_result};
    4.26 -              val _ =
    4.27 -                (case Exn.capture (*sic!*) (restore_attributes run) () of
    4.28 -                  Exn.Res () => ()
    4.29 -                | Exn.Exn exn => toplevel_error exn);
    4.30 -              val _ = status Markup.finished;
    4.31 -            in () end)}
    4.32 -      | _ => NONE);
    4.33 +            val _ = status Markup.running;
    4.34 +            fun run () = f {state = state, args = args, output_result = output_result};
    4.35 +            val _ =
    4.36 +              (case Exn.capture (*sic!*) (restore_attributes run) () of
    4.37 +                Exn.Res () => ()
    4.38 +              | Exn.Exn exn => toplevel_error exn);
    4.39 +            val _ = status Markup.finished;
    4.40 +          in () end)}
    4.41 +    | _ => NONE);
    4.42 +
    4.43 +
    4.44 +(* print_state *)
    4.45 +
    4.46 +val _ =
    4.47 +  register {name = "print_state", pri = Task_Queue.urgent_pri + 2}
    4.48 +    (fn {state = st, output_result, ...} =>
    4.49 +      if Toplevel.is_proof st
    4.50 +      then output_result (Markup.markup (Markup.stateN, []) (Toplevel.string_of_state st))
    4.51 +      else ());
    4.52  
    4.53  end;
     5.1 --- a/src/Tools/jEdit/lib/Tools/jedit	Mon Sep 21 14:56:10 2015 +0200
     5.2 +++ b/src/Tools/jEdit/lib/Tools/jedit	Mon Sep 21 14:56:55 2015 +0200
     5.3 @@ -59,6 +59,7 @@
     5.4    "src/simplifier_trace_window.scala"
     5.5    "src/sledgehammer_dockable.scala"
     5.6    "src/spell_checker.scala"
     5.7 +  "src/state_dockable.scala"
     5.8    "src/structure_matching.scala"
     5.9    "src/symbols_dockable.scala"
    5.10    "src/syslog_dockable.scala"
     6.1 --- a/src/Tools/jEdit/src/Isabelle.props	Mon Sep 21 14:56:10 2015 +0200
     6.2 +++ b/src/Tools/jEdit/src/Isabelle.props	Mon Sep 21 14:56:55 2015 +0200
     6.3 @@ -39,6 +39,7 @@
     6.4    isabelle-raw-output \
     6.5    isabelle-simplifier-trace \
     6.6    isabelle-sledgehammer \
     6.7 +  isabelle-state \
     6.8    isabelle-symbols \
     6.9    isabelle-syslog \
    6.10    isabelle-theories \
    6.11 @@ -65,6 +66,8 @@
    6.12  isabelle-simplifier-trace.title=Simplifier Trace
    6.13  isabelle-sledgehammer.label=Sledgehammer panel
    6.14  isabelle-sledgehammer.title=Sledgehammer
    6.15 +isabelle-state.label=State panel
    6.16 +isabelle-state.title=State
    6.17  isabelle-symbols.label=Symbols panel
    6.18  isabelle-symbols.title=Symbols
    6.19  isabelle-syslog.label=Syslog panel
     7.1 --- a/src/Tools/jEdit/src/dockables.xml	Mon Sep 21 14:56:10 2015 +0200
     7.2 +++ b/src/Tools/jEdit/src/dockables.xml	Mon Sep 21 14:56:55 2015 +0200
     7.3 @@ -35,6 +35,9 @@
     7.4  	<DOCKABLE NAME="isabelle-sledgehammer" MOVABLE="TRUE">
     7.5  		new isabelle.jedit.Sledgehammer_Dockable(view, position);
     7.6  	</DOCKABLE>
     7.7 +	<DOCKABLE NAME="isabelle-state" MOVABLE="TRUE">
     7.8 +		new isabelle.jedit.State_Dockable(view, position);
     7.9 +	</DOCKABLE>
    7.10  	<DOCKABLE NAME="isabelle-symbols" MOVABLE="TRUE">
    7.11  		new isabelle.jedit.Symbols_Dockable(view, position);
    7.12  	</DOCKABLE>
     8.1 --- a/src/Tools/jEdit/src/isabelle.scala	Mon Sep 21 14:56:10 2015 +0200
     8.2 +++ b/src/Tools/jEdit/src/isabelle.scala	Mon Sep 21 14:56:55 2015 +0200
     8.3 @@ -147,6 +147,12 @@
     8.4        case _ => None
     8.5      }
     8.6  
     8.7 +  def state_dockable(view: View): Option[State_Dockable] =
     8.8 +    wm(view).getDockableWindow("isabelle-state") match {
     8.9 +      case dockable: State_Dockable => Some(dockable)
    8.10 +      case _ => None
    8.11 +    }
    8.12 +
    8.13    def symbols_dockable(view: View): Option[Symbols_Dockable] =
    8.14      wm(view).getDockableWindow("isabelle-symbols") match {
    8.15        case dockable: Symbols_Dockable => Some(dockable)
     9.1 --- a/src/Tools/jEdit/src/jEdit.props	Mon Sep 21 14:56:10 2015 +0200
     9.2 +++ b/src/Tools/jEdit/src/jEdit.props	Mon Sep 21 14:56:55 2015 +0200
     9.3 @@ -193,6 +193,7 @@
     9.4  isabelle-query.dock-position=bottom
     9.5  isabelle-simplifier-trace.dock-position=floating
     9.6  isabelle-sledgehammer.dock-position=bottom
     9.7 +isabelle-state.dock-position=right
     9.8  isabelle-symbols.dock-position=bottom
     9.9  isabelle-theories.dock-position=right
    9.10  isabelle.complete-word.label=Complete word
    10.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    10.2 +++ b/src/Tools/jEdit/src/state_dockable.scala	Mon Sep 21 14:56:55 2015 +0200
    10.3 @@ -0,0 +1,101 @@
    10.4 +/*  Title:      Tools/jEdit/src/state_dockable.scala
    10.5 +    Author:     Makarius
    10.6 +
    10.7 +Dockable window for proof state output.
    10.8 +*/
    10.9 +
   10.10 +package isabelle.jedit
   10.11 +
   10.12 +
   10.13 +import isabelle._
   10.14 +
   10.15 +import scala.swing.{Button, CheckBox}
   10.16 +import scala.swing.event.ButtonClicked
   10.17 +
   10.18 +import java.awt.BorderLayout
   10.19 +import java.awt.event.{ComponentEvent, ComponentAdapter}
   10.20 +
   10.21 +import org.gjt.sp.jedit.View
   10.22 +
   10.23 +
   10.24 +class State_Dockable(view: View, position: String) extends Dockable(view, position)
   10.25 +{
   10.26 +  GUI_Thread.require {}
   10.27 +
   10.28 +
   10.29 +  /* text area */
   10.30 +
   10.31 +  val pretty_text_area = new Pretty_Text_Area(view)
   10.32 +  set_content(pretty_text_area)
   10.33 +
   10.34 +  override def detach_operation = pretty_text_area.detach_operation
   10.35 +
   10.36 +  private val print_state =
   10.37 +    new Query_Operation(PIDE.editor, view, "print_state", _ => (),
   10.38 +      (snapshot, results, body) =>
   10.39 +        pretty_text_area.update(snapshot, results, Pretty.separate(body)))
   10.40 +
   10.41 +
   10.42 +  /* resize */
   10.43 +
   10.44 +  private val delay_resize =
   10.45 +    GUI_Thread.delay_first(PIDE.options.seconds("editor_update_delay")) { handle_resize() }
   10.46 +
   10.47 +  addComponentListener(new ComponentAdapter {
   10.48 +    override def componentResized(e: ComponentEvent) { delay_resize.invoke() }
   10.49 +    override def componentShown(e: ComponentEvent) { delay_resize.invoke() }
   10.50 +  })
   10.51 +
   10.52 +  private def handle_resize()
   10.53 +  {
   10.54 +    GUI_Thread.require {}
   10.55 +
   10.56 +    pretty_text_area.resize(
   10.57 +      Font_Info.main(PIDE.options.real("jedit_font_scale") * zoom.factor / 100))
   10.58 +  }
   10.59 +
   10.60 +
   10.61 +  /* controls */
   10.62 +
   10.63 +  private val update = new Button("Update") {
   10.64 +    tooltip = "Update display according to the command at cursor position"
   10.65 +    reactions += { case ButtonClicked(_) => print_state.apply_query(Nil) }
   10.66 +  }
   10.67 +
   10.68 +  private val locate = new Button("Locate") {
   10.69 +    tooltip = "Locate printed command within source text"
   10.70 +    reactions += { case ButtonClicked(_) => print_state.locate_query() }
   10.71 +  }
   10.72 +
   10.73 +  private val zoom = new Font_Info.Zoom_Box { def changed = handle_resize() }
   10.74 +
   10.75 +  private val controls =
   10.76 +    new Wrap_Panel(Wrap_Panel.Alignment.Right)(update, locate,
   10.77 +      pretty_text_area.search_label, pretty_text_area.search_field, zoom)
   10.78 +  add(controls.peer, BorderLayout.NORTH)
   10.79 +
   10.80 +  override def focusOnDefaultComponent { update.requestFocus }
   10.81 +
   10.82 +
   10.83 +  /* main */
   10.84 +
   10.85 +  private val main =
   10.86 +    Session.Consumer[Any](getClass.getName) {
   10.87 +      case _: Session.Global_Options =>
   10.88 +        GUI_Thread.later { handle_resize() }
   10.89 +    }
   10.90 +
   10.91 +  override def init()
   10.92 +  {
   10.93 +    PIDE.session.global_options += main
   10.94 +    handle_resize()
   10.95 +    print_state.activate()
   10.96 +  }
   10.97 +
   10.98 +  override def exit()
   10.99 +  {
  10.100 +    print_state.deactivate()
  10.101 +    PIDE.session.global_options -= main
  10.102 +    delay_resize.revoke()
  10.103 +  }
  10.104 +}