tuned signature;

--- 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 =

--- 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;
 

--- 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)

--- 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;