more general Output.result: allow to update arbitrary properties;
authorwenzelm
Fri Aug 02 22:17:53 2013 +0200 (2013-08-02)
changeset 5285492932931bd82
parent 52853 4ab66773a41f
child 52855 fb1f026c48ff
more general Output.result: allow to update arbitrary properties;
clarified kind/instance of overlay GUI component, with separate output (subject to version as main Output);
src/Pure/General/output.ML
src/Pure/PIDE/markup.ML
src/Pure/PIDE/markup.scala
src/Pure/System/isabelle_process.ML
src/Pure/Tools/find_theorems.ML
src/Tools/jEdit/src/find_dockable.scala
     1.1 --- a/src/Pure/General/output.ML	Fri Aug 02 22:13:31 2013 +0200
     1.2 +++ b/src/Pure/General/output.ML	Fri Aug 02 22:17:53 2013 +0200
     1.3 @@ -35,7 +35,7 @@
     1.4      val prompt_fn: (output -> unit) Unsynchronized.ref
     1.5      val status_fn: (output -> unit) Unsynchronized.ref
     1.6      val report_fn: (output -> unit) Unsynchronized.ref
     1.7 -    val result_fn: (serial * output -> unit) Unsynchronized.ref
     1.8 +    val result_fn: (Properties.T -> output -> unit) Unsynchronized.ref
     1.9      val protocol_message_fn: (Properties.T -> output -> unit) Unsynchronized.ref
    1.10    end
    1.11    val urgent_message: string -> unit
    1.12 @@ -44,7 +44,7 @@
    1.13    val prompt: string -> unit
    1.14    val status: string -> unit
    1.15    val report: string -> unit
    1.16 -  val result: serial * string -> unit
    1.17 +  val result: Properties.T -> string -> unit
    1.18    val protocol_message: Properties.T -> string -> unit
    1.19    val try_protocol_message: Properties.T -> string -> unit
    1.20  end;
    1.21 @@ -102,7 +102,7 @@
    1.22    val prompt_fn = Unsynchronized.ref physical_stdout;
    1.23    val status_fn = Unsynchronized.ref (fn _: output => ());
    1.24    val report_fn = Unsynchronized.ref (fn _: output => ());
    1.25 -  val result_fn = Unsynchronized.ref (fn _: serial * output => ());
    1.26 +  val result_fn = Unsynchronized.ref (fn _: Properties.T => fn _: output => ());
    1.27    val protocol_message_fn: (Properties.T -> output -> unit) Unsynchronized.ref =
    1.28      Unsynchronized.ref (fn props => fn _ => raise Protocol_Message props);
    1.29  end;
    1.30 @@ -116,7 +116,7 @@
    1.31  fun prompt s = ! Internal.prompt_fn (output s);
    1.32  fun status s = ! Internal.status_fn (output s);
    1.33  fun report s = ! Internal.report_fn (output s);
    1.34 -fun result (i, s) = ! Internal.result_fn (i, output s);
    1.35 +fun result props s = ! Internal.result_fn props (output s);
    1.36  fun protocol_message props s = ! Internal.protocol_message_fn props (output s);
    1.37  fun try_protocol_message props s = protocol_message props s handle Protocol_Message _ => ();
    1.38  
     2.1 --- a/src/Pure/PIDE/markup.ML	Fri Aug 02 22:13:31 2013 +0200
     2.2 +++ b/src/Pure/PIDE/markup.ML	Fri Aug 02 22:17:53 2013 +0200
     2.3 @@ -19,6 +19,7 @@
     2.4    val nameN: string
     2.5    val name: string -> T -> T
     2.6    val kindN: string
     2.7 +  val instanceN: string
     2.8    val bindingN: string val binding: T
     2.9    val entityN: string val entity: string -> string -> T
    2.10    val get_entity_kind: T -> string option
    2.11 @@ -118,6 +119,7 @@
    2.12    val finishedN: string val finished: T
    2.13    val failedN: string val failed: T
    2.14    val serialN: string
    2.15 +  val serial_properties: int -> Properties.T
    2.16    val exec_idN: string
    2.17    val initN: string
    2.18    val statusN: string
    2.19 @@ -222,6 +224,8 @@
    2.20  
    2.21  val kindN = "kind";
    2.22  
    2.23 +val instanceN = "instance";
    2.24 +
    2.25  
    2.26  (* formal entities *)
    2.27  
    2.28 @@ -423,6 +427,8 @@
    2.29  (* messages *)
    2.30  
    2.31  val serialN = "serial";
    2.32 +fun serial_properties i = [(serialN, print_int i)];
    2.33 +
    2.34  val exec_idN = "exec_id";
    2.35  
    2.36  val initN = "init";
     3.1 --- a/src/Pure/PIDE/markup.scala	Fri Aug 02 22:13:31 2013 +0200
     3.2 +++ b/src/Pure/PIDE/markup.scala	Fri Aug 02 22:17:53 2013 +0200
     3.3 @@ -18,6 +18,9 @@
     3.4    val KIND = "kind"
     3.5    val Kind = new Properties.String(KIND)
     3.6  
     3.7 +  val INSTANCE = "instance"
     3.8 +  val Instance = new Properties.String(INSTANCE)
     3.9 +
    3.10  
    3.11    /* basic markup */
    3.12  
     4.1 --- a/src/Pure/System/isabelle_process.ML	Fri Aug 02 22:13:31 2013 +0200
     4.2 +++ b/src/Pure/System/isabelle_process.ML	Fri Aug 02 22:17:53 2013 +0200
     4.3 @@ -93,6 +93,8 @@
     4.4  
     4.5  (* output channels *)
     4.6  
     4.7 +val serial_props = Markup.serial_properties o serial;
     4.8 +
     4.9  fun init_channels channel =
    4.10    let
    4.11      val _ = TextIO.StreamIO.setBufferMode (TextIO.getOutstream TextIO.stdOut, IO.LINE_BUF);
    4.12 @@ -103,21 +105,22 @@
    4.13      fun message name props body =
    4.14        Message_Channel.send msg_channel (Message_Channel.message name props body);
    4.15  
    4.16 -    fun standard_message opt_serial name body =
    4.17 +    fun standard_message props name body =
    4.18        if body = "" then ()
    4.19        else
    4.20          message name
    4.21 -          ((case opt_serial of SOME i => cons (Markup.serialN, Markup.print_int i) | _ => I)
    4.22 -            (Position.properties_of (Position.thread_data ()))) body;
    4.23 +          (fold_rev Properties.put props (Position.properties_of (Position.thread_data ()))) body;
    4.24    in
    4.25 -    Output.Internal.status_fn := standard_message NONE Markup.statusN;
    4.26 -    Output.Internal.report_fn := standard_message NONE Markup.reportN;
    4.27 -    Output.Internal.result_fn := (fn (i, s) => standard_message (SOME i) Markup.resultN s);
    4.28 -    Output.Internal.writeln_fn := (fn s => standard_message (SOME (serial ())) Markup.writelnN s);
    4.29 +    Output.Internal.status_fn := standard_message [] Markup.statusN;
    4.30 +    Output.Internal.report_fn := standard_message [] Markup.reportN;
    4.31 +    Output.Internal.result_fn :=
    4.32 +      (fn props => fn s => standard_message (props @ serial_props ()) Markup.resultN s);
    4.33 +    Output.Internal.writeln_fn := (fn s => standard_message (serial_props ()) Markup.writelnN s);
    4.34      Output.Internal.tracing_fn :=
    4.35 -      (fn s => (update_tracing (); standard_message (SOME (serial ())) Markup.tracingN s));
    4.36 -    Output.Internal.warning_fn := (fn s => standard_message (SOME (serial ())) Markup.warningN s);
    4.37 -    Output.Internal.error_fn := (fn (i, s) => standard_message (SOME i) Markup.errorN s);
    4.38 +      (fn s => (update_tracing (); standard_message (serial_props ()) Markup.tracingN s));
    4.39 +    Output.Internal.warning_fn := (fn s => standard_message (serial_props ()) Markup.warningN s);
    4.40 +    Output.Internal.error_fn :=
    4.41 +      (fn (i, s) => standard_message (Markup.serial_properties i) Markup.errorN s);
    4.42      Output.Internal.protocol_message_fn := message Markup.protocolN;
    4.43      Output.Internal.urgent_message_fn := ! Output.Internal.writeln_fn;
    4.44      Output.Internal.prompt_fn := ignore;
     5.1 --- a/src/Pure/Tools/find_theorems.ML	Fri Aug 02 22:13:31 2013 +0200
     5.2 +++ b/src/Pure/Tools/find_theorems.ML	Fri Aug 02 22:17:53 2013 +0200
     5.3 @@ -640,12 +640,15 @@
     5.4  
     5.5  (** print function **)
     5.6  
     5.7 -val _ = Command.print_function "find_theorems"
     5.8 +val find_theoremsN = "find_theorems";
     5.9 +
    5.10 +val _ = Command.print_function find_theoremsN
    5.11    (fn {args, ...} =>
    5.12 -    if null args then NONE
    5.13 -    else
    5.14 +    (case args of
    5.15 +      [instance, query] =>
    5.16        SOME {delay = NONE, pri = 0, persistent = false,
    5.17          print_fn = fn _ => fn st =>
    5.18 -          writeln (cat_lines ("find_theorems" :: args))});
    5.19 +          Output.result [(Markup.kindN, find_theoremsN), (Markup.instanceN, instance)] query}
    5.20 +    | _ => NONE));
    5.21  
    5.22  end;
     6.1 --- a/src/Tools/jEdit/src/find_dockable.scala	Fri Aug 02 22:13:31 2013 +0200
     6.2 +++ b/src/Tools/jEdit/src/find_dockable.scala	Fri Aug 02 22:17:53 2013 +0200
     6.3 @@ -28,16 +28,15 @@
     6.4  
     6.5    /* component state -- owned by Swing thread */
     6.6  
     6.7 -  private val identification = Document_ID.make().toString
     6.8 +  private val FIND_THEOREMS = "find_theorems"
     6.9 +  private val instance = Document_ID.make().toString
    6.10  
    6.11    private var zoom_factor = 100
    6.12 +  private var current_location: Option[Command] = None
    6.13 +  private var current_query: String = ""
    6.14    private var current_snapshot = Document.State.init.snapshot()
    6.15    private var current_state = Command.empty.init_state
    6.16    private var current_output: List[XML.Tree] = Nil
    6.17 -  private var current_location: Option[Command] = None
    6.18 -  private var current_query: String = ""
    6.19 -
    6.20 -  private val FIND_THEOREMS = "find_theorems"
    6.21  
    6.22  
    6.23    /* pretty text area */
    6.24 @@ -54,9 +53,39 @@
    6.25        (Rendering.font_size("jedit_font_scale") * zoom_factor / 100).round)
    6.26    }
    6.27  
    6.28 -  private def handle_output()
    6.29 +  private def handle_update()
    6.30    {
    6.31      Swing_Thread.require()
    6.32 +
    6.33 +    val (new_snapshot, new_state) =
    6.34 +      Document_View(view.getTextArea) match {
    6.35 +        case Some(doc_view) =>
    6.36 +          val snapshot = doc_view.model.snapshot()
    6.37 +          if (!snapshot.is_outdated) {
    6.38 +            current_location match {
    6.39 +              case Some(cmd) =>
    6.40 +                (snapshot, snapshot.state.command_state(snapshot.version, cmd))
    6.41 +              case None =>
    6.42 +                (Document.State.init.snapshot(), Command.empty.init_state)
    6.43 +            }
    6.44 +          }
    6.45 +          else (current_snapshot, current_state)
    6.46 +        case None => (current_snapshot, current_state)
    6.47 +      }
    6.48 +
    6.49 +    val new_output =
    6.50 +      (for {
    6.51 +        (_, XML.Elem(Markup(Markup.RESULT, props), body)) <- new_state.results.entries
    6.52 +        if props.contains((Markup.KIND, FIND_THEOREMS))
    6.53 +        if props.contains((Markup.INSTANCE, instance))
    6.54 +      } yield XML.Elem(Markup(Markup.WRITELN_MESSAGE, Nil), body)).toList
    6.55 +
    6.56 +    if (new_output != current_output)
    6.57 +      pretty_text_area.update(new_snapshot, new_state.results, Pretty.separate(new_output))
    6.58 +
    6.59 +    current_snapshot = new_snapshot
    6.60 +    current_state = new_state
    6.61 +    current_output = new_output
    6.62    }
    6.63  
    6.64    private def clear_overlay()
    6.65 @@ -67,7 +96,7 @@
    6.66        command <- current_location
    6.67        buffer <- JEdit_Lib.jedit_buffer(command.node_name.node)
    6.68        model <- PIDE.document_model(buffer)
    6.69 -    } model.remove_overlay(command, FIND_THEOREMS, List(identification, current_query))
    6.70 +    } model.remove_overlay(command, FIND_THEOREMS, List(instance, current_query))
    6.71  
    6.72      current_location = None
    6.73      current_query = ""
    6.74 @@ -85,7 +114,7 @@
    6.75            case Some(command) =>
    6.76              current_location = Some(command)
    6.77              current_query = query
    6.78 -            doc_view.model.add_overlay(command, FIND_THEOREMS, List(identification, query))
    6.79 +            doc_view.model.add_overlay(command, FIND_THEOREMS, List(instance, query))
    6.80            case None =>
    6.81          }
    6.82        case None =>
    6.83 @@ -120,7 +149,7 @@
    6.84          case changed: Session.Commands_Changed =>
    6.85            current_location match {
    6.86              case Some(command) if changed.commands.contains(command) =>
    6.87 -              Swing_Thread.later { handle_output() }
    6.88 +              Swing_Thread.later { handle_update() }
    6.89              case _ =>
    6.90            }
    6.91          case bad =>