# HG changeset patch # User wenzelm # Date 1372887727 -7200 # Node ID c9a9359e028590efe9ba0e4565ad4623b82c8552 # Parent eb80a16a2b72deccd8721468d503b499b945d81a# Parent 89c5af70553f447bcdbebad8e64f440c4f4ea196 merged diff -r eb80a16a2b72 -r c9a9359e0285 src/Pure/General/symbol.scala --- 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] = diff -r eb80a16a2b72 -r c9a9359e0285 src/Pure/Isar/outer_syntax.ML --- 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; - diff -r eb80a16a2b72 -r c9a9359e0285 src/Pure/PIDE/command.ML --- 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; + diff -r eb80a16a2b72 -r c9a9359e0285 src/Pure/PIDE/command.scala --- 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) diff -r eb80a16a2b72 -r c9a9359e0285 src/Pure/PIDE/document.ML --- 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; diff -r eb80a16a2b72 -r c9a9359e0285 src/Pure/PIDE/document.scala --- 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]] } diff -r eb80a16a2b72 -r c9a9359e0285 src/Pure/ROOT.ML --- 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"; diff -r eb80a16a2b72 -r c9a9359e0285 src/Pure/Syntax/syntax_phases.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; diff -r eb80a16a2b72 -r c9a9359e0285 src/Pure/Thy/thy_load.ML --- 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);