--- a/src/HOL/MicroJava/DFA/Kildall.thy Fri Aug 02 22:36:31 2013 +0200
+++ b/src/HOL/MicroJava/DFA/Kildall.thy Fri Aug 02 22:54:28 2013 +0200
@@ -67,9 +67,8 @@
(** merges **)
-lemma length_merges [rule_format, simp]:
- "\<forall>ss. size(merges f ps ss) = size ss"
- by (induct_tac ps, auto)
+lemma length_merges [simp]: "size(merges f ps ss) = size ss"
+ by (induct ps arbitrary: ss) auto
lemma (in Semilat) merges_preserves_type_lemma:
--- a/src/HOL/MicroJava/J/Conform.thy Fri Aug 02 22:36:31 2013 +0200
+++ b/src/HOL/MicroJava/J/Conform.thy Fri Aug 02 22:54:28 2013 +0200
@@ -137,13 +137,10 @@
apply auto
done
-lemma conf_RefTD [rule_format (no_asm)]:
- "G,h\<turnstile>a'::\<preceq>RefT T --> a' = Null |
+lemma conf_RefTD [rule_format]:
+ "G,h\<turnstile>a'::\<preceq>RefT T \<Longrightarrow> a' = Null \<or>
(\<exists>a obj T'. a' = Addr a \<and> h a = Some obj \<and> obj_ty obj = T' \<and> G\<turnstile>T'\<preceq>RefT T)"
-apply (unfold conf_def)
-apply(induct_tac "a'")
-apply(auto)
-done
+unfolding conf_def by (induct a') auto
lemma conf_NullTD: "G,h\<turnstile>a'::\<preceq>RefT NullT ==> a' = Null"
apply (drule conf_RefTD)
@@ -318,7 +315,7 @@
lemma conforms_hext: "[|(x,(h,l))::\<preceq>(G,lT); h\<le>|h'; G\<turnstile>h h'\<surd> |]
==> (x,(h',l))::\<preceq>(G,lT)"
-by( fast dest: conforms_localD conforms_xcptD elim!: conformsI xconf_hext)
+by (fast dest: conforms_localD conforms_xcptD elim!: conformsI xconf_hext)
lemma conforms_upd_obj:
--- a/src/HOL/MicroJava/J/State.thy Fri Aug 02 22:36:31 2013 +0200
+++ b/src/HOL/MicroJava/J/State.thy Fri Aug 02 22:54:28 2013 +0200
@@ -105,10 +105,7 @@
lemma raise_if_Some2 [simp]:
"raise_if c z (if x = None then Some y else x) \<noteq> None"
-apply (unfold raise_if_def)
-apply(induct_tac "x")
-apply auto
-done
+unfolding raise_if_def by (induct x) auto
lemma raise_if_SomeD [rule_format (no_asm)]:
"raise_if c x y = Some z \<longrightarrow> c \<and> Some z = Some (Addr (XcptRef x)) | y = Some z"
--- a/src/Pure/General/output.ML Fri Aug 02 22:36:31 2013 +0200
+++ b/src/Pure/General/output.ML Fri Aug 02 22:54:28 2013 +0200
@@ -25,7 +25,7 @@
val physical_stderr: output -> unit
val physical_writeln: output -> unit
exception Protocol_Message of Properties.T
- structure Private_Hooks:
+ structure Internal:
sig
val writeln_fn: (output -> unit) Unsynchronized.ref
val urgent_message_fn: (output -> unit) Unsynchronized.ref
@@ -35,7 +35,7 @@
val prompt_fn: (output -> unit) Unsynchronized.ref
val status_fn: (output -> unit) Unsynchronized.ref
val report_fn: (output -> unit) Unsynchronized.ref
- val result_fn: (serial * output -> unit) Unsynchronized.ref
+ val result_fn: (Properties.T -> output -> unit) Unsynchronized.ref
val protocol_message_fn: (Properties.T -> output -> unit) Unsynchronized.ref
end
val urgent_message: string -> unit
@@ -44,7 +44,7 @@
val prompt: string -> unit
val status: string -> unit
val report: string -> unit
- val result: serial * string -> unit
+ val result: Properties.T -> string -> unit
val protocol_message: Properties.T -> string -> unit
val try_protocol_message: Properties.T -> string -> unit
end;
@@ -92,7 +92,7 @@
exception Protocol_Message of Properties.T;
-structure Private_Hooks =
+structure Internal =
struct
val writeln_fn = Unsynchronized.ref physical_writeln;
val urgent_message_fn = Unsynchronized.ref (fn s => ! writeln_fn s);
@@ -102,22 +102,22 @@
val prompt_fn = Unsynchronized.ref physical_stdout;
val status_fn = Unsynchronized.ref (fn _: output => ());
val report_fn = Unsynchronized.ref (fn _: output => ());
- val result_fn = Unsynchronized.ref (fn _: serial * output => ());
+ val result_fn = Unsynchronized.ref (fn _: Properties.T => fn _: output => ());
val protocol_message_fn: (Properties.T -> output -> unit) Unsynchronized.ref =
Unsynchronized.ref (fn props => fn _ => raise Protocol_Message props);
end;
-fun writeln s = ! Private_Hooks.writeln_fn (output s);
-fun urgent_message s = ! Private_Hooks.urgent_message_fn (output s);
-fun tracing s = ! Private_Hooks.tracing_fn (output s);
-fun warning s = ! Private_Hooks.warning_fn (output s);
-fun error_msg' (i, s) = ! Private_Hooks.error_fn (i, output s);
+fun writeln s = ! Internal.writeln_fn (output s);
+fun urgent_message s = ! Internal.urgent_message_fn (output s);
+fun tracing s = ! Internal.tracing_fn (output s);
+fun warning s = ! Internal.warning_fn (output s);
+fun error_msg' (i, s) = ! Internal.error_fn (i, output s);
fun error_msg s = error_msg' (serial (), s);
-fun prompt s = ! Private_Hooks.prompt_fn (output s);
-fun status s = ! Private_Hooks.status_fn (output s);
-fun report s = ! Private_Hooks.report_fn (output s);
-fun result (i, s) = ! Private_Hooks.result_fn (i, output s);
-fun protocol_message props s = ! Private_Hooks.protocol_message_fn props (output s);
+fun prompt s = ! Internal.prompt_fn (output s);
+fun status s = ! Internal.status_fn (output s);
+fun report s = ! Internal.report_fn (output s);
+fun result props s = ! Internal.result_fn props (output s);
+fun protocol_message props s = ! Internal.protocol_message_fn props (output s);
fun try_protocol_message props s = protocol_message props s handle Protocol_Message _ => ();
end;
--- a/src/Pure/PIDE/command.ML Fri Aug 02 22:36:31 2013 +0200
+++ b/src/Pure/PIDE/command.ML Fri Aug 02 22:54:28 2013 +0200
@@ -14,10 +14,11 @@
val eval_result_state: eval -> Toplevel.state
val eval: (unit -> theory) -> Token.T list -> eval -> eval
type print
- val print: bool -> string -> eval -> print list -> print list option
+ val print: bool -> (string * string list) list -> string ->
+ eval -> print list -> print list option
type print_fn = Toplevel.transition -> Toplevel.state -> unit
val print_function: string ->
- ({command_name: string} ->
+ ({command_name: string, args: string list} ->
{delay: Time.time option, pri: int, persistent: bool, print_fn: print_fn} option) -> unit
val no_print_function: string -> unit
type exec = eval * print list
@@ -195,13 +196,13 @@
(* print *)
datatype print = Print of
- {name: string, delay: Time.time option, pri: int, persistent: bool,
+ {name: string, args: string list, delay: Time.time option, pri: int, persistent: bool,
exec_id: Document_ID.exec, print_process: unit memo};
type print_fn = Toplevel.transition -> Toplevel.state -> unit;
type print_function =
- {command_name: string} ->
+ {command_name: string, args: string list} ->
{delay: Time.time option, pri: int, persistent: bool, print_fn: print_fn} option;
local
@@ -221,11 +222,15 @@
fun print_persistent (Print {persistent, ...}) = persistent;
+val overlay_ord = prod_ord string_ord (list_ord string_ord);
+
in
-fun print command_visible command_name eval old_prints =
+fun print command_visible command_overlays command_name eval old_prints =
let
- fun new_print (name, get_pr) =
+ val print_functions = Synchronized.value print_functions;
+
+ fun new_print name args get_pr =
let
fun make_print strict {delay, pri, persistent, print_fn} =
let
@@ -240,11 +245,12 @@
end;
in
Print {
- name = name, delay = delay, pri = pri, persistent = persistent,
+ name = name, args = args, delay = delay, pri = pri, persistent = persistent,
exec_id = exec_id, print_process = memo exec_id process}
end;
+ val params = {command_name = command_name, args = args};
in
- (case Exn.capture (Runtime.controlled_execution get_pr) {command_name = command_name} of
+ (case Exn.capture (Runtime.controlled_execution get_pr) params of
Exn.Res NONE => NONE
| Exn.Res (SOME pr) => SOME (make_print false pr)
| Exn.Exn exn =>
@@ -252,12 +258,19 @@
{delay = NONE, pri = 0, persistent = false, print_fn = fn _ => fn _ => reraise exn}))
end;
+ fun get_print (a, b) =
+ (case find_first (fn Print {name, args, ...} => name = a andalso args = b) old_prints of
+ NONE =>
+ (case AList.lookup (op =) print_functions a of
+ NONE => NONE
+ | SOME get_pr => new_print a b get_pr)
+ | some => some);
+
val new_prints =
if command_visible then
- rev (Synchronized.value print_functions) |> map_filter (fn pr =>
- (case find_first (fn Print {name, ...} => name = fst pr) old_prints of
- NONE => new_print pr
- | some => some))
+ fold (fn (a, _) => cons (a, [])) print_functions command_overlays
+ |> sort_distinct overlay_ord
+ |> map_filter get_print
else filter (fn print => print_finished print andalso print_persistent print) old_prints;
in
if eq_list print_eq (old_prints, new_prints) then NONE else SOME new_prints
@@ -276,7 +289,7 @@
val _ =
print_function "print_state"
- (fn {command_name} =>
+ (fn {command_name, ...} =>
SOME {delay = NONE, pri = 1, persistent = true,
print_fn = fn tr => fn st' =>
let
--- a/src/Pure/PIDE/command.scala Fri Aug 02 22:36:31 2013 +0200
+++ b/src/Pure/PIDE/command.scala Fri Aug 02 22:54:28 2013 +0200
@@ -14,6 +14,9 @@
object Command
{
+ type Edit = (Option[Command], Option[Command])
+
+
/** accumulated results from prover **/
/* results */
--- a/src/Pure/PIDE/document.ML Fri Aug 02 22:36:31 2013 +0200
+++ b/src/Pure/PIDE/document.ML Fri Aug 02 22:54:28 2013 +0200
@@ -9,11 +9,12 @@
sig
val timing: bool Unsynchronized.ref
type node_header = string * Thy_Header.header * string list
+ type overlay = Document_ID.command * string * string list
datatype node_edit =
Clear | (* FIXME unused !? *)
Edits of (Document_ID.command option * Document_ID.command option) list |
Deps of node_header |
- Perspective of bool * Document_ID.command list
+ Perspective of bool * Document_ID.command list * overlay list
type edit = string * node_edit
type state
val init_state: state
@@ -40,12 +41,18 @@
fun err_undef kind id = error ("Undefined " ^ kind ^ ": " ^ Document_ID.print id);
type node_header = string * Thy_Header.header * string list;
-type perspective = bool * Inttab.set * Document_ID.command option;
+
+type perspective =
+ {required: bool, (*required node*)
+ visible: Inttab.set, (*visible commands*)
+ visible_last: Document_ID.command option, (*last visible command*)
+ overlays: (string * string list) list Inttab.table}; (*command id -> print function with args*)
+
structure Entries = Linear_Set(type key = Document_ID.command val ord = int_ord);
abstype node = Node of
{header: node_header, (*master directory, theory header, errors*)
- perspective: perspective, (*required node, visible commands, last visible command*)
+ perspective: perspective, (*command perspective*)
entries: Command.exec option Entries.T, (*command entries with excecutions*)
result: Command.eval option} (*result of last execution*)
and version = Version of node String_Graph.T (*development graph wrt. static imports*)
@@ -57,11 +64,14 @@
fun map_node f (Node {header, perspective, entries, result}) =
make_node (f (header, perspective, entries, result));
-fun make_perspective (required, command_ids) : perspective =
- (required, Inttab.make_set command_ids, try List.last command_ids);
+fun make_perspective (required, command_ids, overlays) : perspective =
+ {required = required,
+ visible = Inttab.make_set command_ids,
+ visible_last = try List.last command_ids,
+ overlays = Inttab.make_list (map (fn (x, y, z) => (x, (y, z))) overlays)};
val no_header = ("", Thy_Header.make ("", Position.none) [] [], ["Bad theory header"]);
-val no_perspective = make_perspective (false, []);
+val no_perspective = make_perspective (false, [], []);
val empty_node = make_node (no_header, no_perspective, Entries.empty, NONE);
val clear_node = map_node (fn (header, _, _, _) => (header, no_perspective, Entries.empty, NONE));
@@ -86,10 +96,11 @@
fun set_perspective args =
map_node (fn (header, _, entries, result) => (header, make_perspective args, entries, result));
-val required_node = #1 o get_perspective;
-val visible_command = Inttab.defined o #2 o get_perspective;
-val visible_last = #3 o get_perspective;
+val required_node = #required o get_perspective;
+val visible_command = Inttab.defined o #visible o get_perspective;
+val visible_last = #visible_last o get_perspective;
val visible_node = is_some o visible_last
+val overlays = Inttab.lookup_list o #overlays o get_perspective;
fun map_entries f =
map_node (fn (header, perspective, entries, result) => (header, perspective, f entries, result));
@@ -124,11 +135,13 @@
(* node edits and associated executions *)
+type overlay = Document_ID.command * string * string list;
+
datatype node_edit =
Clear |
Edits of (Document_ID.command option * Document_ID.command option) list |
Deps of node_header |
- Perspective of bool * Document_ID.command list;
+ Perspective of bool * Document_ID.command list * overlay list;
type edit = string * node_edit;
@@ -429,9 +442,10 @@
SOME (eval, prints) =>
let
val command_visible = visible_command node command_id;
+ val command_overlays = overlays node command_id;
val command_name = the_command_name state command_id;
in
- (case Command.print command_visible command_name eval prints of
+ (case Command.print command_visible command_overlays command_name eval prints of
SOME prints' => assign_update_new (command_id, SOME (eval, prints'))
| NONE => I)
end
@@ -449,15 +463,18 @@
fun illegal_init _ = error "Illegal theory header after end of theory";
-fun new_exec state proper_init command_visible command_id' (assign_update, command_exec, init) =
+fun new_exec state node proper_init command_id' (assign_update, command_exec, init) =
if not proper_init andalso is_none init then NONE
else
let
val (_, (eval, _)) = command_exec;
+
+ val command_visible = visible_command node command_id';
+ val command_overlays = overlays node command_id';
val (command_name, span) = the_command state command_id' ||> Lazy.force;
val eval' = Command.eval (fn () => the_default illegal_init init span) span eval;
- val prints' = perhaps (Command.print command_visible command_name eval') [];
+ val prints' = perhaps (Command.print command_visible command_overlays command_name eval') [];
val exec' = (eval', prints');
val assign_update' = assign_update_new (command_id', SOME exec') assign_update;
@@ -512,7 +529,7 @@
iterate_entries_after common
(fn ((prev, id), _) => fn res =>
if not node_required andalso prev = visible_last node then NONE
- else new_exec state proper_init (visible_command node id) id res) node;
+ else new_exec state node proper_init id res) node;
val assigned_execs =
(node0, updated_execs) |-> iterate_entries_after common
--- a/src/Pure/PIDE/document.scala Fri Aug 02 22:36:31 2013 +0200
+++ b/src/Pure/PIDE/document.scala Fri Aug 02 22:54:28 2013 +0200
@@ -15,11 +15,28 @@
{
/** document structure **/
+ /* overlays -- print functions with arguments */
+
+ type Overlay = (Command, String, List[String])
+
+ object Overlays
+ {
+ val empty = new Overlays(Set.empty)
+ }
+
+ final class Overlays private(rep: Set[Overlay])
+ {
+ def + (o: Overlay) = new Overlays(rep + o)
+ def - (o: Overlay) = new Overlays(rep - o)
+ def dest: List[Overlay] = rep.toList
+ }
+
+
/* individual nodes */
type Edit[A, B] = (Node.Name, Node.Edit[A, B])
type Edit_Text = Edit[Text.Edit, Text.Perspective]
- type Edit_Command = Edit[(Option[Command], Option[Command]), Command.Perspective]
+ type Edit_Command = Edit[Command.Edit, Command.Perspective]
object Node
{
@@ -66,8 +83,9 @@
case class Clear[A, B]() extends Edit[A, B]
case class Edits[A, B](edits: List[A]) extends Edit[A, B]
case class Deps[A, B](header: Header) extends Edit[A, B]
- case class Perspective[A, B](required: Boolean, perspective: B) extends Edit[A, B]
+ case class Perspective[A, B](required: Boolean, visible: B, overlays: Overlays) extends Edit[A, B]
type Perspective_Text = Perspective[Text.Edit, Text.Perspective]
+ type Perspective_Command = Perspective[Command.Edit, Command.Perspective]
def command_starts(commands: Iterator[Command], offset: Text.Offset = 0)
: Iterator[(Command, Text.Offset)] =
@@ -87,7 +105,8 @@
final class Node private(
val header: Node.Header = Node.bad_header("Bad theory header"),
- val perspective: (Boolean, Command.Perspective) = (false, Command.Perspective.empty),
+ val perspective: Node.Perspective_Command =
+ Node.Perspective(false, Command.Perspective.empty, Overlays.empty),
val commands: Linear_Set[Command] = Linear_Set.empty)
{
def clear: Node = new Node(header = header)
@@ -95,11 +114,13 @@
def update_header(new_header: Node.Header): Node =
new Node(new_header, perspective, commands)
- def update_perspective(new_perspective: (Boolean, Command.Perspective)): Node =
+ def update_perspective(new_perspective: Node.Perspective_Command): Node =
new Node(header, new_perspective, commands)
- def same_perspective(other: (Boolean, Command.Perspective)): Boolean =
- perspective._1 == other._1 && (perspective._2 same other._2)
+ def same_perspective(other_perspective: Node.Perspective_Command): Boolean =
+ perspective.required == other_perspective.required &&
+ perspective.visible.same(other_perspective.visible) &&
+ perspective.overlays == other_perspective.overlays
def update_commands(new_commands: Linear_Set[Command]): Node =
new Node(header, perspective, new_commands)
--- a/src/Pure/PIDE/markup.ML Fri Aug 02 22:36:31 2013 +0200
+++ b/src/Pure/PIDE/markup.ML Fri Aug 02 22:54:28 2013 +0200
@@ -19,6 +19,7 @@
val nameN: string
val name: string -> T -> T
val kindN: string
+ val instanceN: string
val bindingN: string val binding: T
val entityN: string val entity: string -> string -> T
val get_entity_kind: T -> string option
@@ -118,6 +119,7 @@
val finishedN: string val finished: T
val failedN: string val failed: T
val serialN: string
+ val serial_properties: int -> Properties.T
val exec_idN: string
val initN: string
val statusN: string
@@ -222,6 +224,8 @@
val kindN = "kind";
+val instanceN = "instance";
+
(* formal entities *)
@@ -423,6 +427,8 @@
(* messages *)
val serialN = "serial";
+fun serial_properties i = [(serialN, print_int i)];
+
val exec_idN = "exec_id";
val initN = "init";
--- a/src/Pure/PIDE/markup.scala Fri Aug 02 22:36:31 2013 +0200
+++ b/src/Pure/PIDE/markup.scala Fri Aug 02 22:54:28 2013 +0200
@@ -18,6 +18,9 @@
val KIND = "kind"
val Kind = new Properties.String(KIND)
+ val INSTANCE = "instance"
+ val Instance = new Properties.String(INSTANCE)
+
/* basic markup */
--- a/src/Pure/PIDE/protocol.ML Fri Aug 02 22:36:31 2013 +0200
+++ b/src/Pure/PIDE/protocol.ML Fri Aug 02 22:54:28 2013 +0200
@@ -56,7 +56,9 @@
val imports' = map (rpair Position.none) imports;
val header = Thy_Header.make (name, Position.none) imports' keywords;
in Document.Deps (master, header, errors) end,
- fn (a :: b, []) => Document.Perspective (bool_atom a, map int_atom b)]))
+ fn (a :: b, c) =>
+ Document.Perspective (bool_atom a, map int_atom b,
+ list (triple int string (list string)) c)]))
end;
val (removed, assign_update, state') = Document.update old_id new_id edits state;
--- a/src/Pure/PIDE/protocol.scala Fri Aug 02 22:36:31 2013 +0200
+++ b/src/Pure/PIDE/protocol.scala Fri Aug 02 22:54:28 2013 +0200
@@ -326,7 +326,7 @@
{ import XML.Encode._
def id: T[Command] = (cmd => long(cmd.id))
def encode_edit(name: Document.Node.Name)
- : T[Document.Node.Edit[(Option[Command], Option[Command]), Command.Perspective]] =
+ : T[Document.Node.Edit[Command.Edit, Command.Perspective]] =
variant(List(
{ case Document.Node.Clear() => (Nil, Nil) }, // FIXME unused !?
{ case Document.Node.Edits(a) => (Nil, list(pair(option(id), option(id)))(a)) },
@@ -340,8 +340,9 @@
option(pair(pair(Encode.string, list(Encode.string)), list(Encode.string))))),
list(Encode.string)))))(
(dir, (name.theory, (imports, (keywords, header.errors)))))) },
- { case Document.Node.Perspective(a, b) =>
- (bool_atom(a) :: b.commands.map(c => long_atom(c.id)), Nil) }))
+ { case Document.Node.Perspective(a, b, c) =>
+ (bool_atom(a) :: b.commands.map(cmd => long_atom(cmd.id)),
+ list(triple(id, Encode.string, list(Encode.string)))(c.dest)) }))
def encode_edits: T[List[Document.Edit_Command]] = list((node_edit: Document.Edit_Command) =>
{
val (name, edit) = node_edit
--- a/src/Pure/System/isabelle_process.ML Fri Aug 02 22:36:31 2013 +0200
+++ b/src/Pure/System/isabelle_process.ML Fri Aug 02 22:54:28 2013 +0200
@@ -93,6 +93,8 @@
(* output channels *)
+val serial_props = Markup.serial_properties o serial;
+
fun init_channels channel =
let
val _ = TextIO.StreamIO.setBufferMode (TextIO.getOutstream TextIO.stdOut, IO.LINE_BUF);
@@ -103,27 +105,25 @@
fun message name props body =
Message_Channel.send msg_channel (Message_Channel.message name props body);
- fun standard_message opt_serial name body =
+ fun standard_message props name body =
if body = "" then ()
else
message name
- ((case opt_serial of SOME i => cons (Markup.serialN, Markup.print_int i) | _ => I)
- (Position.properties_of (Position.thread_data ()))) body;
+ (fold_rev Properties.put props (Position.properties_of (Position.thread_data ()))) body;
in
- Output.Private_Hooks.status_fn := standard_message NONE Markup.statusN;
- Output.Private_Hooks.report_fn := standard_message NONE Markup.reportN;
- Output.Private_Hooks.result_fn := (fn (i, s) => standard_message (SOME i) Markup.resultN s);
- Output.Private_Hooks.writeln_fn :=
- (fn s => standard_message (SOME (serial ())) Markup.writelnN s);
- Output.Private_Hooks.tracing_fn :=
- (fn s => (update_tracing (); standard_message (SOME (serial ())) Markup.tracingN s));
- Output.Private_Hooks.warning_fn :=
- (fn s => standard_message (SOME (serial ())) Markup.warningN s);
- Output.Private_Hooks.error_fn :=
- (fn (i, s) => standard_message (SOME i) Markup.errorN s);
- Output.Private_Hooks.protocol_message_fn := message Markup.protocolN;
- Output.Private_Hooks.urgent_message_fn := ! Output.Private_Hooks.writeln_fn;
- Output.Private_Hooks.prompt_fn := ignore;
+ Output.Internal.status_fn := standard_message [] Markup.statusN;
+ Output.Internal.report_fn := standard_message [] Markup.reportN;
+ Output.Internal.result_fn :=
+ (fn props => fn s => standard_message (props @ serial_props ()) Markup.resultN s);
+ Output.Internal.writeln_fn := (fn s => standard_message (serial_props ()) Markup.writelnN s);
+ Output.Internal.tracing_fn :=
+ (fn s => (update_tracing (); standard_message (serial_props ()) Markup.tracingN s));
+ Output.Internal.warning_fn := (fn s => standard_message (serial_props ()) Markup.warningN s);
+ Output.Internal.error_fn :=
+ (fn (i, s) => standard_message (Markup.serial_properties i) Markup.errorN s);
+ Output.Internal.protocol_message_fn := message Markup.protocolN;
+ Output.Internal.urgent_message_fn := ! Output.Internal.writeln_fn;
+ Output.Internal.prompt_fn := ignore;
message Markup.initN [] (Session.welcome ());
msg_channel
end;
--- a/src/Pure/System/isar.ML Fri Aug 02 22:36:31 2013 +0200
+++ b/src/Pure/System/isar.ML Fri Aug 02 22:54:28 2013 +0200
@@ -156,7 +156,7 @@
fun toplevel_loop in_stream {init = do_init, welcome, sync, secure} =
(Context.set_thread_data NONE;
if do_init then init () else ();
- Output.Private_Hooks.protocol_message_fn := protocol_message;
+ Output.Internal.protocol_message_fn := protocol_message;
if welcome then writeln (Session.welcome ()) else ();
uninterruptible (fn _ => fn () => raw_loop secure (Outer_Syntax.isar in_stream sync)) ());
--- a/src/Pure/Thy/thy_syntax.scala Fri Aug 02 22:36:31 2013 +0200
+++ b/src/Pure/Thy/thy_syntax.scala Fri Aug 02 22:54:28 2013 +0200
@@ -293,7 +293,7 @@
/* main */
def diff_commands(old_cmds: Linear_Set[Command], new_cmds: Linear_Set[Command])
- : List[(Option[Command], Option[Command])] =
+ : List[Command.Edit] =
{
val removed = old_cmds.iterator.filter(!new_cmds.contains(_)).toList
val inserted = new_cmds.iterator.filter(!old_cmds.contains(_)).toList
@@ -311,17 +311,18 @@
case (name, Document.Node.Edits(text_edits)) =>
val commands0 = node.commands
val commands1 = edit_text(text_edits, commands0)
- val commands2 = recover_spans(syntax, name, node.perspective._2, commands1)
+ val commands2 = recover_spans(syntax, name, node.perspective.visible, commands1)
node.update_commands(commands2)
case (_, Document.Node.Deps(_)) => node
- case (name, Document.Node.Perspective(required, text_perspective)) =>
- val perspective = (required, command_perspective(node, text_perspective))
+ case (name, Document.Node.Perspective(required, text_perspective, overlays)) =>
+ val perspective: Document.Node.Perspective_Command =
+ Document.Node.Perspective(required, command_perspective(node, text_perspective), overlays)
if (node.same_perspective(perspective)) node
else
node.update_perspective(perspective).update_commands(
- consolidate_spans(syntax, reparse_limit, name, perspective._2, node.commands))
+ consolidate_spans(syntax, reparse_limit, name, perspective.visible, node.commands))
}
}
@@ -354,8 +355,7 @@
val node2 = (node1 /: edits)(text_edit(syntax, reparse_limit, _, _))
if (!(node.same_perspective(node2.perspective)))
- doc_edits +=
- (name -> Document.Node.Perspective(node2.perspective._1, node2.perspective._2))
+ doc_edits += (name -> node2.perspective)
doc_edits += (name -> Document.Node.Edits(diff_commands(commands, node2.commands)))
--- a/src/Pure/Tools/build.ML Fri Aug 02 22:36:31 2013 +0200
+++ b/src/Pure/Tools/build.ML Fri Aug 02 22:54:28 2013 +0200
@@ -164,7 +164,7 @@
theories |>
(List.app (use_theories_condition last_timing)
|> session_timing name verbose
- |> Unsynchronized.setmp Output.Private_Hooks.protocol_message_fn protocol_message
+ |> Unsynchronized.setmp Output.Internal.protocol_message_fn protocol_message
|> Unsynchronized.setmp Multithreading.max_threads (Options.int options "threads")
|> Exn.capture);
val res2 = Exn.capture Session.finish ();
--- a/src/Pure/Tools/find_theorems.ML Fri Aug 02 22:36:31 2013 +0200
+++ b/src/Pure/Tools/find_theorems.ML Fri Aug 02 22:54:28 2013 +0200
@@ -21,7 +21,7 @@
}
val read_criterion: Proof.context -> string criterion -> term criterion
- val query_parser: (bool * string criterion) list parser
+ val parse_query: string -> (bool * string criterion) list
val xml_of_query: term query -> XML.tree
val query_of_xml: XML.tree -> term query
@@ -496,7 +496,7 @@
end;
-(* print_theorems *)
+(* pretty_theorems *)
fun all_facts_of ctxt =
let
@@ -572,11 +572,12 @@
fun pretty_thm ctxt (thmref, thm) = pretty_theorem ctxt (Internal (thmref, thm));
-fun gen_print_theorems find ctxt opt_goal opt_limit rem_dups raw_criteria =
+fun pretty_theorems ctxt opt_goal opt_limit rem_dups raw_criteria =
let
val criteria = map (apsnd (read_criterion ctxt)) raw_criteria;
- val (foundo, theorems) = find
- {goal = opt_goal, limit = opt_limit, rem_dups = rem_dups, criteria = criteria};
+ val (foundo, theorems) =
+ filter_theorems ctxt (map Internal (all_facts_of ctxt))
+ {goal = opt_goal, limit = opt_limit, rem_dups = rem_dups, criteria = criteria};
val returned = length theorems;
val tally_msg =
@@ -594,10 +595,13 @@
else
[Pretty.str (tally_msg ^ ":"), Pretty.str ""] @
grouped 10 Par_List.map (pretty_theorem ctxt) theorems)
- end |> Pretty.fbreaks |> curry Pretty.blk 0 |> Pretty.writeln;
+ end |> Pretty.fbreaks |> curry Pretty.blk 0;
-fun print_theorems ctxt =
- gen_print_theorems (filter_theorems ctxt (map Internal (all_facts_of ctxt))) ctxt;
+fun pretty_theorems_cmd state opt_lim rem_dups spec =
+ let
+ val ctxt = Toplevel.context_of state;
+ val opt_goal = try (Proof.simple_goal o Toplevel.proof_of) state |> Option.map #goal;
+ in pretty_theorems ctxt opt_goal opt_lim rem_dups spec end;
@@ -619,21 +623,47 @@
(Parse.$$$ "(" |--
Parse.!!! (Scan.option Parse.nat -- Scan.optional (Parse.reserved "with_dups" >> K false) true
--| Parse.$$$ ")")) (NONE, true);
+
+val query_parser = Scan.repeat (((Scan.option Parse.minus >> is_none) -- criterion));
+
in
-val query_parser = Scan.repeat (((Scan.option Parse.minus >> is_none) -- criterion));
+(* FIXME proper wrapper for parser combinator *)
+fun parse_query str =
+ (str ^ ";")
+ |> Outer_Syntax.scan Position.start
+ |> filter Token.is_proper
+ |> Scan.error query_parser
+ |> fst;
val _ =
Outer_Syntax.improper_command @{command_spec "find_theorems"}
"find theorems meeting specified criteria"
- (options -- query_parser
- >> (fn ((opt_lim, rem_dups), spec) =>
- Toplevel.keep (fn state =>
- let
- val ctxt = Toplevel.context_of state;
- val opt_goal = try (Proof.simple_goal o Toplevel.proof_of) state |> Option.map #goal;
- in print_theorems ctxt opt_goal opt_lim rem_dups spec end)));
+ (options -- query_parser >> (fn ((opt_lim, rem_dups), spec) =>
+ Toplevel.keep (fn state =>
+ Pretty.writeln (pretty_theorems_cmd state opt_lim rem_dups spec))));
end;
+
+
+(** print function **)
+
+val find_theoremsN = "find_theorems";
+
+val _ = Command.print_function find_theoremsN
+ (fn {args, ...} =>
+ (case args of
+ [instance, query] =>
+ SOME {delay = NONE, pri = 0, persistent = false,
+ print_fn = fn _ => fn state =>
+ let
+ val msg =
+ Pretty.string_of (pretty_theorems_cmd state NONE false (parse_query query))
+ handle exn =>
+ if Exn.is_interrupt exn then reraise exn
+ else ML_Compiler.exn_message exn; (* FIXME error markup!? *)
+ in Output.result [(Markup.kindN, find_theoremsN), (Markup.instanceN, instance)] msg end}
+ | _ => NONE));
+
end;
--- a/src/Pure/Tools/proof_general.ML Fri Aug 02 22:36:31 2013 +0200
+++ b/src/Pure/Tools/proof_general.ML Fri Aug 02 22:54:28 2013 +0200
@@ -261,14 +261,14 @@
| s => Output.physical_writeln (enclose bg en (prefix_lines prfx s)));
fun setup_messages () =
- (Output.Private_Hooks.writeln_fn := message "" "" "";
- Output.Private_Hooks.status_fn := (fn _ => ());
- Output.Private_Hooks.report_fn := (fn _ => ());
- Output.Private_Hooks.urgent_message_fn := message (special "I") (special "J") "";
- Output.Private_Hooks.tracing_fn := message (special "I" ^ special "V") (special "J") "";
- Output.Private_Hooks.warning_fn := message (special "K") (special "L") "### ";
- Output.Private_Hooks.error_fn := (fn (_, s) => message (special "M") (special "N") "*** " s);
- Output.Private_Hooks.prompt_fn := (fn s => Output.physical_stdout (render s ^ special "S")));
+ (Output.Internal.writeln_fn := message "" "" "";
+ Output.Internal.status_fn := (fn _ => ());
+ Output.Internal.report_fn := (fn _ => ());
+ Output.Internal.urgent_message_fn := message (special "I") (special "J") "";
+ Output.Internal.tracing_fn := message (special "I" ^ special "V") (special "J") "";
+ Output.Internal.warning_fn := message (special "K") (special "L") "### ";
+ Output.Internal.error_fn := (fn (_, s) => message (special "M") (special "N") "*** " s);
+ Output.Internal.prompt_fn := (fn s => Output.physical_stdout (render s ^ special "S")));
(* notification *)
--- a/src/Tools/WWW_Find/find_theorems.ML Fri Aug 02 22:36:31 2013 +0200
+++ b/src/Tools/WWW_Find/find_theorems.ML Fri Aug 02 22:54:28 2013 +0200
@@ -16,12 +16,7 @@
val args = Symtab.lookup arg_data;
val query_str = the_default "" (args "query");
- fun get_query () =
- (query_str ^ ";")
- |> Outer_Syntax.scan Position.start
- |> filter Token.is_proper
- |> Scan.error Find_Theorems.query_parser
- |> fst;
+ fun get_query () = Find_Theorems.parse_query query_str;
val limit = case args "limit" of
NONE => default_limit
--- a/src/Tools/jEdit/lib/Tools/jedit Fri Aug 02 22:36:31 2013 +0200
+++ b/src/Tools/jEdit/lib/Tools/jedit Fri Aug 02 22:54:28 2013 +0200
@@ -13,6 +13,7 @@
"src/document_model.scala"
"src/document_view.scala"
"src/documentation_dockable.scala"
+ "src/find_dockable.scala"
"src/fold_handling.scala"
"src/graphview_dockable.scala"
"src/html_panel.scala"
--- a/src/Tools/jEdit/src/Isabelle.props Fri Aug 02 22:36:31 2013 +0200
+++ b/src/Tools/jEdit/src/Isabelle.props Fri Aug 02 22:54:28 2013 +0200
@@ -31,6 +31,7 @@
plugin.isabelle.jedit.Plugin.menu.label=Isabelle
plugin.isabelle.jedit.Plugin.menu= \
isabelle.documentation-panel \
+ isabelle.find-panel \
isabelle.monitor-panel \
isabelle.output-panel \
isabelle.protocol-panel \
@@ -41,6 +42,7 @@
isabelle.theories-panel \
isabelle.timing-panel
isabelle.documentation-panel.label=Documentation panel
+isabelle.find-panel.label=Find panel
isabelle.monitor-panel.label=Monitor panel
isabelle.output-panel.label=Output panel
isabelle.protocol-panel.label=Protocol panel
@@ -52,6 +54,7 @@
isabelle.timing-panel.label=Timing panel
#dockables
+isabelle-find.title=Find
isabelle-graphview.title=Graphview
isabelle-info.title=Info
isabelle-monitor.title=Monitor
--- a/src/Tools/jEdit/src/actions.xml Fri Aug 02 22:36:31 2013 +0200
+++ b/src/Tools/jEdit/src/actions.xml Fri Aug 02 22:54:28 2013 +0200
@@ -27,6 +27,11 @@
wm.addDockableWindow("isabelle-readme");
</CODE>
</ACTION>
+ <ACTION NAME="isabelle.find-panel">
+ <CODE>
+ wm.addDockableWindow("isabelle-find");
+ </CODE>
+ </ACTION>
<ACTION NAME="isabelle.output-panel">
<CODE>
wm.addDockableWindow("isabelle-output");
--- a/src/Tools/jEdit/src/dockables.xml Fri Aug 02 22:36:31 2013 +0200
+++ b/src/Tools/jEdit/src/dockables.xml Fri Aug 02 22:54:28 2013 +0200
@@ -20,6 +20,9 @@
<DOCKABLE NAME="isabelle-output" MOVABLE="TRUE">
new isabelle.jedit.Output_Dockable(view, position);
</DOCKABLE>
+ <DOCKABLE NAME="isabelle-find" MOVABLE="TRUE">
+ new isabelle.jedit.Find_Dockable(view, position);
+ </DOCKABLE>
<DOCKABLE NAME="isabelle-info" MOVABLE="TRUE">
new isabelle.jedit.Info_Dockable(view, position);
</DOCKABLE>
--- a/src/Tools/jEdit/src/document_model.scala Fri Aug 02 22:36:31 2013 +0200
+++ b/src/Tools/jEdit/src/document_model.scala Fri Aug 02 22:54:28 2013 +0200
@@ -77,8 +77,28 @@
}
+ /* overlays */
+
+ private var overlays = Document.Overlays.empty
+
+ def add_overlay(command: Command, name: String, args: List[String])
+ {
+ Swing_Thread.required()
+ overlays += ((command, name, args))
+ PIDE.flush_buffers()
+ }
+
+ def remove_overlay(command: Command, name: String, args: List[String])
+ {
+ Swing_Thread.required()
+ overlays -= ((command, name, args))
+ PIDE.flush_buffers()
+ }
+
+
/* perspective */
+ // owned by Swing thread
private var _node_required = false
def node_required: Boolean = _node_required
def node_required_=(b: Boolean)
@@ -91,21 +111,21 @@
}
}
+ val empty_perspective: Document.Node.Perspective_Text =
+ Document.Node.Perspective(false, Text.Perspective.empty, Document.Overlays.empty)
+
def node_perspective(): Document.Node.Perspective_Text =
{
Swing_Thread.require()
- val perspective =
- if (Isabelle.continuous_checking) {
- (node_required, Text.Perspective(
- for {
- doc_view <- PIDE.document_views(buffer)
- range <- doc_view.perspective().ranges
- } yield range))
- }
- else (false, Text.Perspective.empty)
-
- Document.Node.Perspective(perspective._1, perspective._2)
+ if (Isabelle.continuous_checking) {
+ Document.Node.Perspective(node_required, Text.Perspective(
+ for {
+ doc_view <- PIDE.document_views(buffer)
+ range <- doc_view.perspective().ranges
+ } yield range), overlays)
+ }
+ else empty_perspective
}
@@ -143,8 +163,7 @@
private object pending_edits // owned by Swing thread
{
private val pending = new mutable.ListBuffer[Text.Edit]
- private var last_perspective: Document.Node.Perspective_Text =
- Document.Node.Perspective(node_required, Text.Perspective.empty)
+ private var last_perspective = empty_perspective
def snapshot(): List[Text.Edit] = pending.toList
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/jEdit/src/find_dockable.scala Fri Aug 02 22:54:28 2013 +0200
@@ -0,0 +1,217 @@
+/* Title: Tools/jEdit/src/find_dockable.scala
+ Author: Makarius
+
+Dockable window for "find" dialog.
+*/
+
+package isabelle.jedit
+
+
+import isabelle._
+
+import scala.actors.Actor._
+
+import scala.swing.{FlowPanel, Button, Component}
+import scala.swing.event.ButtonClicked
+
+import java.awt.BorderLayout
+import java.awt.event.{ComponentEvent, ComponentAdapter}
+
+import org.gjt.sp.jedit.View
+import org.gjt.sp.jedit.gui.HistoryTextArea
+
+
+class Find_Dockable(view: View, position: String) extends Dockable(view, position)
+{
+ Swing_Thread.require()
+
+
+ /* component state -- owned by Swing thread */
+
+ private val FIND_THEOREMS = "find_theorems"
+ private val instance = Document_ID.make().toString
+
+ private var zoom_factor = 100
+ private var current_location: Option[Command] = None
+ private var current_query: String = ""
+ private var current_snapshot = Document.State.init.snapshot()
+ private var current_state = Command.empty.init_state
+ private var current_output: List[XML.Tree] = Nil
+
+
+ /* pretty text area */
+
+ val pretty_text_area = new Pretty_Text_Area(view)
+ set_content(pretty_text_area)
+
+
+ private def handle_resize()
+ {
+ Swing_Thread.require()
+
+ pretty_text_area.resize(Rendering.font_family(),
+ (Rendering.font_size("jedit_font_scale") * zoom_factor / 100).round)
+ }
+
+ private def handle_update()
+ {
+ Swing_Thread.require()
+
+ val (new_snapshot, new_state) =
+ Document_View(view.getTextArea) match {
+ case Some(doc_view) =>
+ val snapshot = doc_view.model.snapshot()
+ if (!snapshot.is_outdated) {
+ current_location match {
+ case Some(cmd) =>
+ (snapshot, snapshot.state.command_state(snapshot.version, cmd))
+ case None =>
+ (Document.State.init.snapshot(), Command.empty.init_state)
+ }
+ }
+ else (current_snapshot, current_state)
+ case None => (current_snapshot, current_state)
+ }
+
+ val new_output =
+ (for {
+ (_, XML.Elem(Markup(Markup.RESULT, props), body)) <- new_state.results.entries
+ if props.contains((Markup.KIND, FIND_THEOREMS))
+ if props.contains((Markup.INSTANCE, instance))
+ } yield XML.Elem(Markup(Markup.WRITELN_MESSAGE, Nil), body)).toList
+
+ if (new_output != current_output)
+ pretty_text_area.update(new_snapshot, new_state.results, Pretty.separate(new_output))
+
+ current_snapshot = new_snapshot
+ current_state = new_state
+ current_output = new_output
+ }
+
+ private def clear_overlay()
+ {
+ Swing_Thread.require()
+
+ for {
+ command <- current_location
+ buffer <- JEdit_Lib.jedit_buffer(command.node_name.node)
+ model <- PIDE.document_model(buffer)
+ } model.remove_overlay(command, FIND_THEOREMS, List(instance, current_query))
+
+ current_location = None
+ current_query = ""
+ }
+
+ private def apply_query(query: String)
+ {
+ Swing_Thread.require()
+
+ clear_overlay()
+ Document_View(view.getTextArea) match {
+ case Some(doc_view) =>
+ val snapshot = doc_view.model.snapshot()
+ snapshot.node.command_at(doc_view.text_area.getCaretPosition).map(_._1) match {
+ case Some(command) =>
+ current_location = Some(command)
+ current_query = query
+ doc_view.model.add_overlay(command, FIND_THEOREMS, List(instance, query))
+ case None =>
+ }
+ case None =>
+ }
+ }
+
+ private def locate_query()
+ {
+ Swing_Thread.require()
+
+ current_location match {
+ case Some(command) =>
+ val snapshot = PIDE.session.snapshot(command.node_name)
+ val commands = snapshot.node.commands
+ if (commands.contains(command)) {
+ val sources = commands.iterator.takeWhile(_ != command).map(_.source)
+ val (line, column) = ((1, 1) /: sources)(Symbol.advance_line_column)
+ Hyperlink(command.node_name.node, line, column).follow(view)
+ }
+ case None =>
+ }
+ }
+
+
+ /* main actor */
+
+ private val main_actor = actor {
+ loop {
+ react {
+ case _: Session.Global_Options =>
+ Swing_Thread.later { handle_resize() }
+ case changed: Session.Commands_Changed =>
+ current_location match {
+ case Some(command) if changed.commands.contains(command) =>
+ Swing_Thread.later { handle_update() }
+ case _ =>
+ }
+ case bad =>
+ java.lang.System.err.println("Find_Dockable: ignoring bad message " + bad)
+ }
+ }
+ }
+
+ override def init()
+ {
+ Swing_Thread.require()
+
+ PIDE.session.global_options += main_actor
+ PIDE.session.commands_changed += main_actor
+ handle_resize()
+ }
+
+ override def exit()
+ {
+ Swing_Thread.require()
+
+ PIDE.session.global_options -= main_actor
+ PIDE.session.commands_changed -= main_actor
+ delay_resize.revoke()
+ }
+
+
+ /* resize */
+
+ private val delay_resize =
+ Swing_Thread.delay_first(PIDE.options.seconds("editor_update_delay")) { handle_resize() }
+
+ addComponentListener(new ComponentAdapter {
+ override def componentResized(e: ComponentEvent) { delay_resize.invoke() }
+ })
+
+
+ /* controls */
+
+ private val query = new HistoryTextArea("isabelle-find-theorems") {
+ { val max = getPreferredSize; max.width = Integer.MAX_VALUE; setMaximumSize(max) }
+ setColumns(25)
+ setRows(1)
+ }
+
+ private val query_wrapped = Component.wrap(query)
+
+ private val find = new Button("Find") {
+ tooltip = "Find theorems meeting specified criteria"
+ reactions += { case ButtonClicked(_) => apply_query(query.getText) }
+ }
+
+ private val locate = new Button("Locate") {
+ tooltip = "Locate context of current query within source text"
+ reactions += { case ButtonClicked(_) => locate_query() }
+ }
+
+ private val zoom = new GUI.Zoom_Box(factor => { zoom_factor = factor; handle_resize() }) {
+ tooltip = "Zoom factor for output font size"
+ }
+
+ private val controls =
+ new FlowPanel(FlowPanel.Alignment.Right)(query_wrapped, find, locate, zoom)
+ add(controls.peer, BorderLayout.NORTH)
+}
--- a/src/Tools/jEdit/src/output_dockable.scala Fri Aug 02 22:36:31 2013 +0200
+++ b/src/Tools/jEdit/src/output_dockable.scala Fri Aug 02 22:54:28 2013 +0200
@@ -135,30 +135,31 @@
/* controls */
- private val zoom = new GUI.Zoom_Box(factor => { zoom_factor = factor; handle_resize() })
- zoom.tooltip = "Zoom factor for basic font size"
+ private val zoom = new GUI.Zoom_Box(factor => { zoom_factor = factor; handle_resize() }) {
+ tooltip = "Zoom factor for output font size"
+ }
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
}
- auto_update.selected = do_update
- auto_update.tooltip = "Indicate automatic update following cursor movement"
private val update = new Button("Update") {
+ tooltip = "Update display according to the command at cursor position"
reactions += { case ButtonClicked(_) => handle_update(true, None) }
}
- update.tooltip = "Update display according to the command at cursor position"
private val detach = new Button("Detach") {
+ tooltip = "Detach window with static copy of current output"
reactions += {
case ButtonClicked(_) =>
Info_Dockable(view, current_snapshot,
current_state.results, Pretty.separate(current_output))
}
}
- detach.tooltip = "Detach window with static copy of current output"
- private val controls = new FlowPanel(FlowPanel.Alignment.Right)(zoom, auto_update, update, detach)
+ private val controls = new FlowPanel(FlowPanel.Alignment.Right)(auto_update, update, detach, zoom)
add(controls.peer, BorderLayout.NORTH)
}
--- a/src/Tools/try.ML Fri Aug 02 22:36:31 2013 +0200
+++ b/src/Tools/try.ML Fri Aug 02 22:54:28 2013 +0200
@@ -117,7 +117,7 @@
fun print_function ((name, (weight, auto, tool)): tool) =
Command.print_function name
- (fn {command_name} =>
+ (fn {command_name, ...} =>
if Keyword.is_theory_goal command_name andalso Options.default_bool auto then
SOME
{delay = SOME (seconds (Options.default_real @{option auto_time_start})),