--- a/src/Pure/General/symbol.scala Wed Jul 03 20:41:41 2013 +0200
+++ b/src/Pure/General/symbol.scala Wed Jul 03 23:42:07 2013 +0200
@@ -111,7 +111,12 @@
/* decoding offsets */
- class Index(text: CharSequence)
+ object Index
+ {
+ def apply(text: CharSequence): Index = new Index(text)
+ }
+
+ final class Index private(text: CharSequence)
{
sealed case class Entry(chr: Int, sym: Int)
val index: Array[Entry] =
--- a/src/Pure/Isar/outer_syntax.ML Wed Jul 03 20:41:41 2013 +0200
+++ b/src/Pure/Isar/outer_syntax.ML Wed Jul 03 23:42:07 2013 +0200
@@ -34,8 +34,9 @@
val parse: Position.T -> string -> Toplevel.transition list
type isar
val isar: TextIO.instream -> bool -> isar
- val span_cmts: Token.T list -> Token.T list
- val read_span: outer_syntax -> Token.T list -> Toplevel.transition
+ val side_comments: Token.T list -> Token.T list
+ val command_reports: outer_syntax -> Token.T -> (Position.report * string) list
+ val read_spans: outer_syntax -> Token.T list -> Toplevel.transition list
end;
structure Outer_Syntax: OUTER_SYNTAX =
@@ -279,55 +280,29 @@
(* side-comments *)
-local
-
fun cmts (t1 :: t2 :: toks) =
if Token.keyword_with (fn s => s = "--") t1 then t2 :: cmts toks
else cmts (t2 :: toks)
| cmts _ = [];
-in
+val side_comments = filter Token.is_proper #> cmts;
+
+
+(* read commands *)
-val span_cmts = filter Token.is_proper #> cmts;
+fun command_reports outer_syntax tok =
+ if Token.is_command tok then
+ let val name = Token.content_of tok in
+ (case lookup_commands outer_syntax name of
+ NONE => []
+ | SOME cmd => [((Token.position_of tok, command_markup false (name, cmd)), "")])
+ end
+ else [];
+
+fun read_spans outer_syntax toks =
+ Source.of_list toks
+ |> toplevel_source false NONE (K (lookup_commands outer_syntax))
+ |> Source.exhaust;
end;
-
-(* read command span -- fail-safe *)
-
-fun read_span outer_syntax toks =
- let
- val commands = lookup_commands outer_syntax;
-
- val proper_range = Position.set_range (Command.proper_range toks);
- val pos =
- (case find_first Token.is_command toks of
- SOME tok => Token.position_of tok
- | NONE => proper_range);
-
- fun command_reports tok =
- if Token.is_command tok then
- let val name = Token.content_of tok in
- (case commands name of
- NONE => []
- | SOME cmd => [((Token.position_of tok, command_markup false (name, cmd)), "")])
- end
- else [];
-
- val (is_malformed, token_reports) = Thy_Syntax.reports_of_tokens toks;
- val _ = Position.reports_text (token_reports @ maps command_reports toks);
- in
- if is_malformed then Toplevel.malformed pos "Malformed command syntax"
- else
- (case Source.exhaust (toplevel_source false NONE (K commands) (Source.of_list toks)) of
- [tr] =>
- if Keyword.is_control (Toplevel.name_of tr) then
- Toplevel.malformed pos "Illegal control command"
- else tr
- | [] => Toplevel.ignored (Position.set_range (Command.range toks))
- | _ => Toplevel.malformed proper_range "Exactly one command expected")
- handle ERROR msg => Toplevel.malformed proper_range msg
- end;
-
-end;
-
--- a/src/Pure/PIDE/command.ML Wed Jul 03 20:41:41 2013 +0200
+++ b/src/Pure/PIDE/command.ML Wed Jul 03 23:42:07 2013 +0200
@@ -6,21 +6,31 @@
signature COMMAND =
sig
- val range: Token.T list -> Position.range
- val proper_range: Token.T list -> Position.range
+ type span = Token.T list
+ val range: span -> Position.range
+ val proper_range: span -> Position.range
type 'a memo
val memo: (unit -> 'a) -> 'a memo
val memo_value: 'a -> 'a memo
val memo_eval: 'a memo -> 'a
val memo_result: 'a memo -> 'a
- val run_command: Toplevel.transition * Token.T list ->
- Toplevel.state * bool -> (Toplevel.state * bool) * unit lazy
+ val read: span -> Toplevel.transition
+ val eval: span -> Toplevel.transition ->
+ Toplevel.state * {malformed: bool} -> {failed: bool} * (Toplevel.state * {malformed: bool})
+ type print = {name: string, pri: int, pr: unit lazy}
+ val print: Toplevel.state -> Toplevel.transition -> Toplevel.state -> print list
+ type print_function =
+ {old_state: Toplevel.state, tr: Toplevel.transition, state: Toplevel.state} ->
+ (unit -> unit) option
+ val print_function: string -> int -> print_function -> unit
end;
structure Command: COMMAND =
struct
-(* span range *)
+(* source *)
+
+type span = Token.T list;
val range = Token.position_range_of;
val proper_range = Token.position_range_of o #1 o take_suffix Token.is_improper;
@@ -57,7 +67,36 @@
end;
-(* run command *)
+(* read *)
+
+fun read span =
+ let
+ val outer_syntax = #2 (Outer_Syntax.get_syntax ());
+ val command_reports = Outer_Syntax.command_reports outer_syntax;
+
+ val proper_range = Position.set_range (proper_range span);
+ val pos =
+ (case find_first Token.is_command span of
+ SOME tok => Token.position_of tok
+ | NONE => proper_range);
+
+ val (is_malformed, token_reports) = Thy_Syntax.reports_of_tokens span;
+ val _ = Position.reports_text (token_reports @ maps command_reports span);
+ in
+ if is_malformed then Toplevel.malformed pos "Malformed command syntax"
+ else
+ (case Outer_Syntax.read_spans outer_syntax span of
+ [tr] =>
+ if Keyword.is_control (Toplevel.name_of tr) then
+ Toplevel.malformed pos "Illegal control command"
+ else tr
+ | [] => Toplevel.ignored (Position.set_range (range span))
+ | _ => Toplevel.malformed proper_range "Exactly one command expected")
+ handle ERROR msg => Toplevel.malformed proper_range msg
+ end;
+
+
+(* eval *)
local
@@ -67,11 +106,11 @@
(fn () => Toplevel.command_exception int tr st); ([], SOME st))
else Toplevel.command_errors int tr st;
-fun check_cmts tr cmts st =
+fun check_cmts span tr st' =
Toplevel.setmp_thread_position tr
- (fn () => cmts
- |> maps (fn cmt =>
- (Thy_Output.check_text (Token.source_position_of cmt) st; [])
+ (fn () =>
+ Outer_Syntax.side_comments span |> maps (fn cmt =>
+ (Thy_Output.check_text (Token.source_position_of cmt) st'; [])
handle exn => ML_Compiler.exn_messages_ids exn)) ();
fun proof_status tr st =
@@ -79,16 +118,11 @@
SOME prf => Toplevel.status tr (Proof.status_markup prf)
| NONE => ());
-val no_print = Lazy.value ();
-
-fun print_state tr st =
- (Lazy.lazy o Toplevel.setmp_thread_position tr)
- (fn () => Toplevel.print_state false st);
-
in
-fun run_command (tr, cmts) (st, malformed) =
- if malformed then ((Toplevel.toplevel, malformed), no_print)
+fun eval span tr (st, {malformed}) =
+ if malformed then
+ ({failed = true}, (Toplevel.toplevel, {malformed = malformed}))
else
let
val malformed' = Toplevel.is_malformed tr;
@@ -98,7 +132,7 @@
val _ = Multithreading.interrupted ();
val _ = Toplevel.status tr Markup.running;
val (errs1, result) = run (is_init orelse is_proof) (Toplevel.set_print false tr) st;
- val errs2 = (case result of NONE => [] | SOME st' => check_cmts tr cmts st');
+ val errs2 = (case result of NONE => [] | SOME st' => check_cmts span tr st');
val errs = errs1 @ errs2;
val _ = Toplevel.status tr Markup.finished;
val _ = List.app (Future.error_msg (Toplevel.pos_of tr)) errs;
@@ -108,17 +142,61 @@
let
val _ = if null errs then Exn.interrupt () else ();
val _ = Toplevel.status tr Markup.failed;
- in ((st, malformed'), no_print) end
+ in ({failed = true}, (st, {malformed = malformed'})) end
| SOME st' =>
let
val _ = proof_status tr st';
- val do_print =
- not is_init andalso
- (Toplevel.print_of tr orelse (is_proof andalso Toplevel.is_proof st'));
- in ((st', malformed'), if do_print then print_state tr st' else no_print) end)
+ in ({failed = false}, (st', {malformed = malformed'})) end)
end;
end;
+
+(* print *)
+
+type print_function =
+ {old_state: Toplevel.state, tr: Toplevel.transition, state: Toplevel.state} ->
+ (unit -> unit) option;
+
+type print = {name: string, pri: int, pr: unit lazy};
+
+local
+
+val print_functions =
+ Synchronized.var "Command.print_functions" ([]: (string * (int * print_function)) list);
+
+fun output_error tr exn =
+ List.app (Future.error_msg (Toplevel.pos_of tr)) (ML_Compiler.exn_messages_ids exn);
+
+fun print_error tr f x =
+ (Toplevel.setmp_thread_position tr o Runtime.controlled_execution) f x
+ handle exn => output_error tr exn;
+
+in
+
+fun print st tr st' =
+ rev (Synchronized.value print_functions) |> map_filter (fn (name, (pri, f)) =>
+ (case Exn.capture (Runtime.controlled_execution f) {old_state = st, tr = tr, state = st'} of
+ Exn.Res NONE => NONE
+ | Exn.Res (SOME pr) => SOME {name = name, pri = pri, pr = (Lazy.lazy o print_error tr) pr}
+ | Exn.Exn exn => SOME {name = name, pri = pri, pr = Lazy.lazy (fn () => output_error tr exn)}));
+
+fun print_function name pri f =
+ Synchronized.change print_functions (fn funs =>
+ (if not (AList.defined (op =) funs name) then ()
+ else warning ("Redefining command print function: " ^ quote name);
+ AList.update (op =) (name, (pri, f)) funs));
+
end;
+val _ = print_function "print_state" 0 (fn {tr, state, ...} =>
+ let
+ val is_init = Toplevel.is_init tr;
+ val is_proof = Keyword.is_proof (Toplevel.name_of tr);
+ val do_print =
+ not is_init andalso
+ (Toplevel.print_of tr orelse (is_proof andalso Toplevel.is_proof state));
+ in if do_print then SOME (fn () => Toplevel.print_state false state) else NONE end);
+
+end;
+
--- a/src/Pure/PIDE/command.scala Wed Jul 03 20:41:41 2013 +0200
+++ b/src/Pure/PIDE/command.scala Wed Jul 03 23:42:07 2013 +0200
@@ -217,7 +217,7 @@
id + "/" + (if (is_command) name else if (is_ignored) "IGNORED" else "MALFORMED")
- /* source text */
+ /* source */
def length: Int = source.length
val range: Text.Range = Text.Range(0, length)
@@ -227,7 +227,7 @@
def source(range: Text.Range): String = source.substring(range.start, range.stop)
- lazy val symbol_index = new Symbol.Index(source)
+ lazy val symbol_index = Symbol.Index(source)
def decode(i: Text.Offset): Text.Offset = symbol_index.decode(i)
def decode(r: Text.Range): Text.Range = symbol_index.decode(r)
--- a/src/Pure/PIDE/document.ML Wed Jul 03 20:41:41 2013 +0200
+++ b/src/Pure/PIDE/document.ML Wed Jul 03 23:42:07 2013 +0200
@@ -63,12 +63,13 @@
type perspective = (command_id -> bool) * command_id option;
structure Entries = Linear_Set(type key = command_id val ord = int_ord);
-type exec = ((Toplevel.state * bool) * unit lazy) Command.memo; (*eval/print process*)
-val no_exec = Command.memo_value ((Toplevel.toplevel, false), Lazy.value ());
+type exec = ((Toplevel.state * {malformed: bool}) * Command.print list) Command.memo;
+ (*eval/print process*)
+val no_exec = Command.memo_value ((Toplevel.toplevel, {malformed = false}), []);
abstype node = Node of
{header: node_header, (*master directory, theory header, errors*)
- perspective: perspective, (*visible commands, last*)
+ perspective: perspective, (*visible commands, last visible command*)
entries: (exec_id * exec) option Entries.T * bool, (*command entries with excecutions, stable*)
result: exec option} (*result of last execution*)
and version = Version of node String_Graph.T (*development graph wrt. static imports*)
@@ -323,20 +324,18 @@
fun start_execution state =
let
- fun run node command_id exec =
- let
- val (_, print) = Command.memo_eval exec;
- val _ =
- if visible_command node command_id
- then ignore (Lazy.future Future.default_params print)
- else ();
- in () end;
+ fun execute exec =
+ Command.memo_eval exec
+ |> (fn (_, print) =>
+ print |> List.app (fn {name, pri, pr} =>
+ Lazy.future {name = name, group = NONE, deps = [], pri = pri, interrupts = true} pr
+ |> ignore));
val (version_id, group, running) = execution_of state;
val _ =
(singleton o Future.forks)
- {name = "execution", group = SOME group, deps = [], pri = ~2, interrupts = true}
+ {name = "Document.execution", group = SOME group, deps = [], pri = ~2, interrupts = true}
(fn () =>
(OS.Process.sleep (seconds 0.02);
nodes_of (the_version state version_id) |> String_Graph.schedule
@@ -348,9 +347,9 @@
{name = "theory:" ^ name, group = SOME (Future.new_group (SOME group)),
deps = map (Future.task_of o #2) deps, pri = ~2, interrupts = false}
(fn () =>
- iterate_entries (fn ((_, id), opt_exec) => fn () =>
+ iterate_entries (fn (_, opt_exec) => fn () =>
(case opt_exec of
- SOME (_, exec) => if ! running then SOME (run node id exec) else NONE
+ SOME (_, exec) => if ! running then SOME (execute exec) else NONE
| NONE => NONE)) node ()))));
in () end;
@@ -434,32 +433,32 @@
else (common, flags)
end;
-fun illegal_init _ = error "Illegal theory header after end of theory";
-
-fun new_exec state proper_init command_id' (execs, command_exec, init) =
+fun new_exec state proper_init command_visible command_id' (execs, command_exec, init) =
if not proper_init andalso is_none init then NONE
else
let
val (name, span) = the_command state command_id' ||> Lazy.force;
+ fun illegal_init _ = error "Illegal theory header after end of theory";
val (modify_init, init') =
if Keyword.is_theory_begin name then
(Toplevel.modify_init (fn () => the_default illegal_init init span), NONE)
else (I, init);
val exec_id' = new_id ();
val exec_id'_string = print_id exec_id';
- val cmd =
+ val read =
Position.setmp_thread_data (Position.id_only exec_id'_string)
(fn () =>
- let
- val tr =
- Outer_Syntax.read_span (#2 (Outer_Syntax.get_syntax ())) span
- |> modify_init
- |> Toplevel.put_id exec_id'_string;
- val cmts = Outer_Syntax.span_cmts span;
- in (tr, cmts) end);
+ Command.read span
+ |> modify_init
+ |> Toplevel.put_id exec_id'_string);
val exec' =
Command.memo (fn () =>
- Command.run_command (cmd ()) (fst (Command.memo_result (snd (snd command_exec)))));
+ let
+ val ((st, malformed), _) = Command.memo_result (snd (snd command_exec));
+ val tr = read ();
+ val ({failed}, (st', malformed')) = Command.eval span tr (st, malformed);
+ val print = if failed orelse not command_visible then [] else Command.print st tr st';
+ in ((st', malformed'), print) end);
val command_exec' = (command_id', (exec_id', exec'));
in SOME (command_exec' :: execs, command_exec', init') end;
@@ -468,7 +467,6 @@
fun update (old_id: version_id) (new_id: version_id) edits state =
let
val old_version = the_version state old_id;
- val _ = Time.now (); (* FIXME odd workaround for polyml-5.4.0/x86_64 *)
val new_version = timeit "Document.edit_nodes" (fn () => fold edit_nodes edits old_version);
val nodes = nodes_of new_version;
@@ -485,7 +483,7 @@
let
val imports = map (apsnd Future.join) deps;
val updated_imports = exists (is_some o #3 o #1 o #2) imports;
- val required = is_required name;
+ val node_required = is_required name;
in
if updated_imports orelse AList.defined (op =) edits name orelse
not (stable_entries node) orelse not (finished_theory node)
@@ -498,18 +496,18 @@
forall (fn (name, (_, node)) => check_theory true name node) imports;
val last_visible = visible_last node;
- val (common, (visible, initial)) =
+ val (common, (still_visible, initial)) =
if updated_imports then (NONE, (true, true))
else last_common state last_visible node0 node;
val common_command_exec = the_default_entry node common;
val (new_execs, (command_id', (_, exec')), _) =
([], common_command_exec, if initial then SOME init else NONE) |>
- (visible orelse required) ?
+ (still_visible orelse node_required) ?
iterate_entries_after common
(fn ((prev, id), _) => fn res =>
- if not required andalso prev = last_visible then NONE
- else new_exec state proper_init id res) node;
+ if not node_required andalso prev = last_visible then NONE
+ else new_exec state proper_init (visible_command node id) id res) node;
val no_execs =
iterate_entries_after common
@@ -551,7 +549,7 @@
(** global state **)
-val global_state = Synchronized.var "Document" init_state;
+val global_state = Synchronized.var "Document.global_state" init_state;
fun state () = Synchronized.value global_state;
val change_state = Synchronized.change global_state;
--- a/src/Pure/PIDE/document.scala Wed Jul 03 20:41:41 2013 +0200
+++ b/src/Pure/PIDE/document.scala Wed Jul 03 23:42:07 2013 +0200
@@ -278,9 +278,14 @@
def revert(i: Text.Offset): Text.Offset
def revert(range: Text.Range): Text.Range
def eq_content(other: Snapshot): Boolean
- def cumulate_markup[A](range: Text.Range, info: A, elements: Option[Set[String]],
+ def cumulate_markup[A](
+ range: Text.Range,
+ info: A,
+ elements: Option[Set[String]],
result: Command.State => PartialFunction[(A, Text.Markup), A]): Stream[Text.Info[A]]
- def select_markup[A](range: Text.Range, elements: Option[Set[String]],
+ def select_markup[A](
+ range: Text.Range,
+ elements: Option[Set[String]],
result: Command.State => PartialFunction[Text.Markup, A]): Stream[Text.Info[A]]
}
--- a/src/Pure/ROOT.ML Wed Jul 03 20:41:41 2013 +0200
+++ b/src/Pure/ROOT.ML Wed Jul 03 23:42:07 2013 +0200
@@ -262,10 +262,10 @@
use "System/isabelle_system.ML";
use "Thy/term_style.ML";
use "Thy/thy_output.ML";
-use "PIDE/command.ML";
use "Isar/outer_syntax.ML";
use "General/graph_display.ML";
use "Thy/present.ML";
+use "PIDE/command.ML";
use "Thy/thy_load.ML";
use "Thy/thy_info.ML";
use "PIDE/document.ML";
--- a/src/Pure/Syntax/syntax_phases.ML Wed Jul 03 20:41:41 2013 +0200
+++ b/src/Pure/Syntax/syntax_phases.ML Wed Jul 03 23:42:07 2013 +0200
@@ -318,7 +318,8 @@
(("Ambiguous input" ^ Position.here (Position.reset_range pos) ^
"\nproduces " ^ string_of_int len ^ " parse trees" ^
(if len <= limit then "" else " (" ^ string_of_int limit ^ " displayed)") ^ ":") ::
- map (Pretty.string_of o Parser.pretty_parsetree) (take limit pts))];
+ map (Pretty.string_of o Pretty.item o single o Parser.pretty_parsetree)
+ (take limit pts))];
in (ambig_msgs, map (parsetree_to_ast ctxt ast_tr) pts) end;
@@ -389,7 +390,7 @@
val checked = map snd (proper_results results');
val checked_len = length checked;
- val show_term = Syntax.string_of_term (Config.put Printer.show_brackets true ctxt);
+ val pretty_term = Syntax.pretty_term (Config.put Printer.show_brackets true ctxt);
in
if checked_len = 0 then
report_result ctxt pos []
@@ -408,7 +409,8 @@
(("Ambiguous input\n" ^ string_of_int checked_len ^ " terms are type correct" ^
(if checked_len <= limit then ""
else " (" ^ string_of_int limit ^ " displayed)") ^ ":") ::
- map show_term (take limit checked))))))]
+ map (Pretty.string_of o Pretty.item o single o pretty_term)
+ (take limit checked))))))]
end handle ERROR msg => parse_failed ctxt pos msg kind)
end;
--- a/src/Pure/Thy/thy_load.ML Wed Jul 03 20:41:41 2013 +0200
+++ b/src/Pure/Thy/thy_load.ML Wed Jul 03 23:42:07 2013 +0200
@@ -217,7 +217,7 @@
let
fun prepare_span span =
Thy_Syntax.span_content span
- |> Outer_Syntax.read_span (#2 (Outer_Syntax.get_syntax ()))
+ |> Command.read
|> Toplevel.modify_init init
|> (fn tr => Toplevel.put_timing (last_timing tr) tr);