1.1 --- a/src/Pure/Isar/outer_syntax.ML	Wed Jul 03 15:19:36 2013 +0200
     1.2 +++ b/src/Pure/Isar/outer_syntax.ML	Wed Jul 03 16:19:57 2013 +0200
     1.3 @@ -34,7 +34,6 @@
     1.4    val parse: Position.T -> string -> Toplevel.transition list
     1.5    type isar
     1.6    val isar: TextIO.instream -> bool -> isar
     1.7 -  val span_cmts: Token.T list -> Token.T list
     1.8    val read_span: outer_syntax -> Token.T list -> Toplevel.transition
     1.9  end;
    1.10  
    1.11 @@ -277,22 +276,6 @@
    1.12    |> toplevel_source term (SOME true) lookup_commands_dynamic;
    1.13  
    1.14  
    1.15 -(* side-comments *)
    1.16 -
    1.17 -local
    1.18 -
    1.19 -fun cmts (t1 :: t2 :: toks) =
    1.20 -      if Token.keyword_with (fn s => s = "--") t1 then t2 :: cmts toks
    1.21 -      else cmts (t2 :: toks)
    1.22 -  | cmts _ = [];
    1.23 -
    1.24 -in
    1.25 -
    1.26 -val span_cmts = filter Token.is_proper #> cmts;
    1.27 -
    1.28 -end;
    1.29 -
    1.30 -
    1.31  (* read command span -- fail-safe *)
    1.32  
    1.33  fun read_span outer_syntax toks =

     2.1 --- a/src/Pure/PIDE/command.ML	Wed Jul 03 15:19:36 2013 +0200
     2.2 +++ b/src/Pure/PIDE/command.ML	Wed Jul 03 16:19:57 2013 +0200
     2.3 @@ -6,21 +6,26 @@
     2.4  
     2.5  signature COMMAND =
     2.6  sig
     2.7 -  val range: Token.T list -> Position.range
     2.8 -  val proper_range: Token.T list -> Position.range
     2.9 +  type span = Token.T list
    2.10 +  val range: span -> Position.range
    2.11 +  val proper_range: span -> Position.range
    2.12    type 'a memo
    2.13    val memo: (unit -> 'a) -> 'a memo
    2.14    val memo_value: 'a -> 'a memo
    2.15    val memo_eval: 'a memo -> 'a
    2.16    val memo_result: 'a memo -> 'a
    2.17 -  val run_command: Toplevel.transition * Token.T list ->
    2.18 -    Toplevel.state * bool -> (Toplevel.state * bool) * unit lazy
    2.19 +  val eval: span -> Toplevel.transition ->
    2.20 +    Toplevel.state * {malformed: bool} -> {failed: bool} * (Toplevel.state * {malformed: bool})
    2.21 +  val no_print: unit lazy
    2.22 +  val print: Toplevel.transition -> Toplevel.state -> unit lazy
    2.23  end;
    2.24  
    2.25  structure Command: COMMAND =
    2.26  struct
    2.27  
    2.28 -(* span range *)
    2.29 +(* source *)
    2.30 +
    2.31 +type span = Token.T list;
    2.32  
    2.33  val range = Token.position_range_of;
    2.34  val proper_range = Token.position_range_of o #1 o take_suffix Token.is_improper;
    2.35 @@ -57,7 +62,30 @@
    2.36  end;
    2.37  
    2.38  
    2.39 -(* run command *)
    2.40 +(* side-comments *)
    2.41 +
    2.42 +local
    2.43 +
    2.44 +fun cmts (t1 :: t2 :: toks) =
    2.45 +      if Token.keyword_with (fn s => s = "--") t1 then t2 :: cmts toks
    2.46 +      else cmts (t2 :: toks)
    2.47 +  | cmts _ = [];
    2.48 +
    2.49 +val span_cmts = filter Token.is_proper #> cmts;
    2.50 +
    2.51 +in
    2.52 +
    2.53 +fun check_cmts span tr st' =
    2.54 +  Toplevel.setmp_thread_position tr
    2.55 +    (fn () =>
    2.56 +      span_cmts span |> maps (fn cmt =>
    2.57 +        (Thy_Output.check_text (Token.source_position_of cmt) st'; [])
    2.58 +          handle exn => ML_Compiler.exn_messages_ids exn)) ();
    2.59 +
    2.60 +end;
    2.61 +
    2.62 +
    2.63 +(* eval *)
    2.64  
    2.65  local
    2.66  
    2.67 @@ -67,28 +95,16 @@
    2.68        (fn () => Toplevel.command_exception int tr st); ([], SOME st))
    2.69    else Toplevel.command_errors int tr st;
    2.70  
    2.71 -fun check_cmts tr cmts st =
    2.72 -  Toplevel.setmp_thread_position tr
    2.73 -    (fn () => cmts
    2.74 -      |> maps (fn cmt =>
    2.75 -        (Thy_Output.check_text (Token.source_position_of cmt) st; [])
    2.76 -          handle exn => ML_Compiler.exn_messages_ids exn)) ();
    2.77 -
    2.78  fun proof_status tr st =
    2.79    (case try Toplevel.proof_of st of
    2.80      SOME prf => Toplevel.status tr (Proof.status_markup prf)
    2.81    | NONE => ());
    2.82  
    2.83 -val no_print = Lazy.value ();
    2.84 -
    2.85 -fun print_state tr st =
    2.86 -  (Lazy.lazy o Toplevel.setmp_thread_position tr)
    2.87 -    (fn () => Toplevel.print_state false st);
    2.88 -
    2.89  in
    2.90  
    2.91 -fun run_command (tr, cmts) (st, malformed) =
    2.92 -  if malformed then ((Toplevel.toplevel, malformed), no_print)
    2.93 +fun eval span tr (st, {malformed}) =
    2.94 +  if malformed then
    2.95 +    ({failed = true}, (Toplevel.toplevel, {malformed = malformed}))
    2.96    else
    2.97      let
    2.98        val malformed' = Toplevel.is_malformed tr;
    2.99 @@ -98,7 +114,7 @@
   2.100        val _ = Multithreading.interrupted ();
   2.101        val _ = Toplevel.status tr Markup.running;
   2.102        val (errs1, result) = run (is_init orelse is_proof) (Toplevel.set_print false tr) st;
   2.103 -      val errs2 = (case result of NONE => [] | SOME st' => check_cmts tr cmts st');
   2.104 +      val errs2 = (case result of NONE => [] | SOME st' => check_cmts span tr st');
   2.105        val errs = errs1 @ errs2;
   2.106        val _ = Toplevel.status tr Markup.finished;
   2.107        val _ = List.app (Future.error_msg (Toplevel.pos_of tr)) errs;
   2.108 @@ -108,17 +124,33 @@
   2.109            let
   2.110              val _ = if null errs then Exn.interrupt () else ();
   2.111              val _ = Toplevel.status tr Markup.failed;
   2.112 -          in ((st, malformed'), no_print) end
   2.113 +          in ({failed = true}, (st, {malformed = malformed'})) end
   2.114        | SOME st' =>
   2.115            let
   2.116              val _ = proof_status tr st';
   2.117 -            val do_print =
   2.118 -              not is_init andalso
   2.119 -                (Toplevel.print_of tr orelse (is_proof andalso Toplevel.is_proof st'));
   2.120 -          in ((st', malformed'), if do_print then print_state tr st' else no_print) end)
   2.121 +          in ({failed = false}, (st', {malformed = malformed'})) end)
   2.122      end;
   2.123  
   2.124  end;
   2.125  
   2.126 +
   2.127 +(* print *)
   2.128 +
   2.129 +val no_print = Lazy.value ();
   2.130 +
   2.131 +fun print tr st' =
   2.132 +  let
   2.133 +    val is_init = Toplevel.is_init tr;
   2.134 +    val is_proof = Keyword.is_proof (Toplevel.name_of tr);
   2.135 +    val do_print =
   2.136 +      not is_init andalso
   2.137 +        (Toplevel.print_of tr orelse (is_proof andalso Toplevel.is_proof st'));
   2.138 +  in
   2.139 +    if do_print then
   2.140 +      (Lazy.lazy o Toplevel.setmp_thread_position tr)
   2.141 +        (fn () => Toplevel.print_state false st')
   2.142 +    else no_print
   2.143 +  end;
   2.144 +
   2.145  end;
   2.146  

     3.1 --- a/src/Pure/PIDE/command.scala	Wed Jul 03 15:19:36 2013 +0200
     3.2 +++ b/src/Pure/PIDE/command.scala	Wed Jul 03 16:19:57 2013 +0200
     3.3 @@ -217,7 +217,7 @@
     3.4      id + "/" + (if (is_command) name else if (is_ignored) "IGNORED" else "MALFORMED")
     3.5  
     3.6  
     3.7 -  /* source text */
     3.8 +  /* source */
     3.9  
    3.10    def length: Int = source.length
    3.11    val range: Text.Range = Text.Range(0, length)

     4.1 --- a/src/Pure/PIDE/document.ML	Wed Jul 03 15:19:36 2013 +0200
     4.2 +++ b/src/Pure/PIDE/document.ML	Wed Jul 03 16:19:57 2013 +0200
     4.3 @@ -63,8 +63,8 @@
     4.4  type perspective = (command_id -> bool) * command_id option;
     4.5  structure Entries = Linear_Set(type key = command_id val ord = int_ord);
     4.6  
     4.7 -type exec = ((Toplevel.state * bool) * unit lazy) Command.memo;  (*eval/print process*)
     4.8 -val no_exec = Command.memo_value ((Toplevel.toplevel, false), Lazy.value ());
     4.9 +type exec = ((Toplevel.state * {malformed: bool}) * unit lazy) Command.memo;  (*eval/print process*)
    4.10 +val no_exec = Command.memo_value ((Toplevel.toplevel, {malformed = false}), Lazy.value ());
    4.11  
    4.12  abstype node = Node of
    4.13   {header: node_header,  (*master directory, theory header, errors*)
    4.14 @@ -447,19 +447,20 @@
    4.15          else (I, init);
    4.16        val exec_id' = new_id ();
    4.17        val exec_id'_string = print_id exec_id';
    4.18 -      val cmd =
    4.19 +      val read =
    4.20          Position.setmp_thread_data (Position.id_only exec_id'_string)
    4.21            (fn () =>
    4.22 -            let
    4.23 -              val tr =
    4.24 -                Outer_Syntax.read_span (#2 (Outer_Syntax.get_syntax ())) span
    4.25 -                |> modify_init
    4.26 -                |> Toplevel.put_id exec_id'_string;
    4.27 -              val cmts = Outer_Syntax.span_cmts span;
    4.28 -            in (tr, cmts) end);
    4.29 +            Outer_Syntax.read_span (#2 (Outer_Syntax.get_syntax ())) span
    4.30 +            |> modify_init
    4.31 +            |> Toplevel.put_id exec_id'_string);
    4.32        val exec' =
    4.33          Command.memo (fn () =>
    4.34 -          Command.run_command (cmd ()) (fst (Command.memo_result (snd (snd command_exec)))));
    4.35 +          let
    4.36 +            val (st, _) = Command.memo_result (snd (snd command_exec));
    4.37 +            val tr = read ();
    4.38 +            val ({failed}, (st', malformed')) = Command.eval span tr st;
    4.39 +            val print = if failed then Command.no_print else Command.print tr st';
    4.40 +          in ((st', malformed'), print) end);
    4.41        val command_exec' = (command_id', (exec_id', exec'));
    4.42      in SOME (command_exec' :: execs, command_exec', init') end;
    4.43