# HG changeset patch
# User wenzelm
# Date 1372863515 -7200
# Node ID a4a102237ded89867b07245eb89ad4fc2d31901d
# Parent  2193d2c7f58610ed4a3a17b69c70ea0951dbc642
tuned signature;

diff -r 2193d2c7f586 -r a4a102237ded src/Pure/Isar/outer_syntax.ML
--- a/src/Pure/Isar/outer_syntax.ML	Wed Jul 03 16:19:57 2013 +0200
+++ b/src/Pure/Isar/outer_syntax.ML	Wed Jul 03 16:58:35 2013 +0200
@@ -34,7 +34,9 @@
   val parse: Position.T -> string -> Toplevel.transition list
   type isar
   val isar: TextIO.instream -> bool -> isar
-  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 =
@@ -276,41 +278,31 @@
   |> toplevel_source term (SOME true) lookup_commands_dynamic;
 
 
-(* read command span -- fail-safe *)
-
-fun read_span outer_syntax toks =
-  let
-    val commands = lookup_commands outer_syntax;
+(* side-comments *)
 
-    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 cmts (t1 :: t2 :: toks) =
+      if Token.keyword_with (fn s => s = "--") t1 then t2 :: cmts toks
+      else cmts (t2 :: toks)
+  | cmts _ = [];
+
+val side_comments = filter Token.is_proper #> cmts;
+
+
+(* read commands *)
 
-    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 [];
+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 [];
 
-    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;
+fun read_spans outer_syntax toks =
+  Source.of_list toks
+  |> toplevel_source false NONE (K (lookup_commands outer_syntax))
+  |> Source.exhaust;
 
 end;
 
diff -r 2193d2c7f586 -r a4a102237ded src/Pure/PIDE/command.ML
--- a/src/Pure/PIDE/command.ML	Wed Jul 03 16:19:57 2013 +0200
+++ b/src/Pure/PIDE/command.ML	Wed Jul 03 16:58:35 2013 +0200
@@ -14,6 +14,7 @@
   val memo_value: 'a -> 'a memo
   val memo_eval: 'a memo -> 'a
   val memo_result: 'a memo -> 'a
+  val read: span -> Toplevel.transition
   val eval: span -> Toplevel.transition ->
     Toplevel.state * {malformed: bool} -> {failed: bool} * (Toplevel.state * {malformed: bool})
   val no_print: unit lazy
@@ -62,27 +63,33 @@
 end;
 
 
-(* side-comments *)
-
-local
+(* read *)
 
-fun cmts (t1 :: t2 :: toks) =
-      if Token.keyword_with (fn s => s = "--") t1 then t2 :: cmts toks
-      else cmts (t2 :: toks)
-  | cmts _ = [];
+fun read span =
+  let
+    val outer_syntax = #2 (Outer_Syntax.get_syntax ());
+    val command_reports = Outer_Syntax.command_reports outer_syntax;
 
-val span_cmts = filter Token.is_proper #> cmts;
+    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);
 
-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;
+    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 *)
@@ -95,6 +102,13 @@
       (fn () => Toplevel.command_exception int tr st); ([], SOME st))
   else Toplevel.command_errors int tr st;
 
+fun check_cmts span tr st' =
+  Toplevel.setmp_thread_position tr
+    (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 =
   (case try Toplevel.proof_of st of
     SOME prf => Toplevel.status tr (Proof.status_markup prf)
diff -r 2193d2c7f586 -r a4a102237ded src/Pure/PIDE/document.ML
--- a/src/Pure/PIDE/document.ML	Wed Jul 03 16:19:57 2013 +0200
+++ b/src/Pure/PIDE/document.ML	Wed Jul 03 16:58:35 2013 +0200
@@ -450,7 +450,7 @@
       val read =
         Position.setmp_thread_data (Position.id_only exec_id'_string)
           (fn () =>
-            Outer_Syntax.read_span (#2 (Outer_Syntax.get_syntax ())) span
+            Command.read span
             |> modify_init
             |> Toplevel.put_id exec_id'_string);
       val exec' =
diff -r 2193d2c7f586 -r a4a102237ded src/Pure/ROOT.ML
--- a/src/Pure/ROOT.ML	Wed Jul 03 16:19:57 2013 +0200
+++ b/src/Pure/ROOT.ML	Wed Jul 03 16:58:35 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 2193d2c7f586 -r a4a102237ded src/Pure/Thy/thy_load.ML
--- a/src/Pure/Thy/thy_load.ML	Wed Jul 03 16:19:57 2013 +0200
+++ b/src/Pure/Thy/thy_load.ML	Wed Jul 03 16:58:35 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);