# HG changeset patch # User wenzelm # Date 1372861197 -7200 # Node ID 2193d2c7f58610ed4a3a17b69c70ea0951dbc642 # Parent 98475be0b1a211e2b7e4e2c069345f75aaa99824 tuned signature; diff -r 98475be0b1a2 -r 2193d2c7f586 src/Pure/Isar/outer_syntax.ML --- a/src/Pure/Isar/outer_syntax.ML Wed Jul 03 15:19:36 2013 +0200 +++ b/src/Pure/Isar/outer_syntax.ML Wed Jul 03 16:19:57 2013 +0200 @@ -34,7 +34,6 @@ 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 end; @@ -277,22 +276,6 @@ |> toplevel_source term (SOME true) lookup_commands_dynamic; -(* 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 span_cmts = filter Token.is_proper #> cmts; - -end; - - (* read command span -- fail-safe *) fun read_span outer_syntax toks = diff -r 98475be0b1a2 -r 2193d2c7f586 src/Pure/PIDE/command.ML --- a/src/Pure/PIDE/command.ML Wed Jul 03 15:19:36 2013 +0200 +++ b/src/Pure/PIDE/command.ML Wed Jul 03 16:19:57 2013 +0200 @@ -6,21 +6,26 @@ 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 eval: span -> Toplevel.transition -> + Toplevel.state * {malformed: bool} -> {failed: bool} * (Toplevel.state * {malformed: bool}) + val no_print: unit lazy + val print: Toplevel.transition -> Toplevel.state -> unit lazy 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 +62,30 @@ end; -(* run command *) +(* 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 _ = []; + +val span_cmts = filter Token.is_proper #> cmts; + +in + +fun check_cmts span tr st' = + Toplevel.setmp_thread_position tr + (fn () => + span_cmts span |> maps (fn cmt => + (Thy_Output.check_text (Token.source_position_of cmt) st'; []) + handle exn => ML_Compiler.exn_messages_ids exn)) (); + +end; + + +(* eval *) local @@ -67,28 +95,16 @@ (fn () => Toplevel.command_exception int tr st); ([], SOME st)) else Toplevel.command_errors int tr st; -fun check_cmts tr cmts st = - Toplevel.setmp_thread_position tr - (fn () => cmts - |> 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 = (case try Toplevel.proof_of st of 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 +114,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 +124,33 @@ 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 *) + +val no_print = Lazy.value (); + +fun print tr st' = + 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 st')); + in + if do_print then + (Lazy.lazy o Toplevel.setmp_thread_position tr) + (fn () => Toplevel.print_state false st') + else no_print + end; + end; diff -r 98475be0b1a2 -r 2193d2c7f586 src/Pure/PIDE/command.scala --- a/src/Pure/PIDE/command.scala Wed Jul 03 15:19:36 2013 +0200 +++ b/src/Pure/PIDE/command.scala Wed Jul 03 16:19:57 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) diff -r 98475be0b1a2 -r 2193d2c7f586 src/Pure/PIDE/document.ML --- a/src/Pure/PIDE/document.ML Wed Jul 03 15:19:36 2013 +0200 +++ b/src/Pure/PIDE/document.ML Wed Jul 03 16:19:57 2013 +0200 @@ -63,8 +63,8 @@ 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}) * unit lazy) Command.memo; (*eval/print process*) +val no_exec = Command.memo_value ((Toplevel.toplevel, {malformed = false}), Lazy.value ()); abstype node = Node of {header: node_header, (*master directory, theory header, errors*) @@ -447,19 +447,20 @@ 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); + Outer_Syntax.read_span (#2 (Outer_Syntax.get_syntax ())) 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, _) = Command.memo_result (snd (snd command_exec)); + val tr = read (); + val ({failed}, (st', malformed')) = Command.eval span tr st; + val print = if failed then Command.no_print else Command.print tr st'; + in ((st', malformed'), print) end); val command_exec' = (command_id', (exec_id', exec')); in SOME (command_exec' :: execs, command_exec', init') end;