# HG changeset patch
# User wenzelm
# Date 1314988179 -7200
# Node ID 5bec9c15ef29e4411e0e110f80c802407218df78
# Parent  17dbd9d9db380a47fe94a108036fac7ce1216a3e
more direct Token.range_pos and Outer_Syntax.read_command, bypassing Thy_Syntax.span;

diff -r 17dbd9d9db38 -r 5bec9c15ef29 src/Pure/Isar/outer_syntax.ML
--- a/src/Pure/Isar/outer_syntax.ML	Fri Sep 02 19:25:44 2011 +0200
+++ b/src/Pure/Isar/outer_syntax.ML	Fri Sep 02 20:29:39 2011 +0200
@@ -34,7 +34,6 @@
   val process_file: Path.T -> theory -> theory
   type isar
   val isar: TextIO.instream -> bool -> isar
-  val read_span: outer_syntax -> Thy_Syntax.span -> Toplevel.transition * bool
   val read_element: outer_syntax -> (unit -> theory) -> Thy_Syntax.element ->
     (Toplevel.transition * Toplevel.transition list) list
   val read_command: Position.T -> string -> Toplevel.transition
@@ -255,17 +254,16 @@
 
 val not_singleton = "Exactly one command expected";
 
-fun read_span outer_syntax span =
+fun read_span outer_syntax toks =
   let
     val commands = lookup_commands outer_syntax;
-    val range_pos = Position.set_range (Thy_Syntax.span_range span);
-    val toks = Thy_Syntax.span_content span;
+    val range_pos = Position.set_range (Token.range toks);
     val _ = List.app Thy_Syntax.report_token toks;
   in
     (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 range_pos "Illegal control command", true)
+          (Toplevel.malformed (Toplevel.pos_of tr) "Illegal control command", true)
         else (tr, true)
     | [] => (Toplevel.ignored range_pos, false)
     | _ => (Toplevel.malformed range_pos not_singleton, true))
@@ -274,19 +272,19 @@
 
 fun read_element outer_syntax init {head, proof, proper_proof} =
   let
-    val (tr, proper_head) = read_span outer_syntax head |>> Toplevel.modify_init init;
-    val proof_trs = map (read_span outer_syntax) proof |> filter #2 |> map #1;
+    val read = read_span outer_syntax o Thy_Syntax.span_content;
+    val (tr, proper_head) = read head |>> Toplevel.modify_init init;
+    val proof_trs = map read proof |> filter #2 |> map #1;
   in
     if proper_head andalso proper_proof then [(tr, proof_trs)]
     else map (rpair []) (if proper_head then tr :: proof_trs else proof_trs)
   end;
 
 fun read_command pos str =
-  let val (lexs, outer_syntax) = get_syntax () in
-    (case Thy_Syntax.parse_spans lexs pos str of
-      [span] => #1 (read_span outer_syntax span)
-    | _ => Toplevel.malformed pos not_singleton)
-  end;
+  let
+    val (lexs, outer_syntax) = get_syntax ();
+    val toks = Thy_Syntax.parse_tokens lexs pos str;
+  in #1 (read_span outer_syntax toks) end;
 
 end;
 
diff -r 17dbd9d9db38 -r 5bec9c15ef29 src/Pure/Isar/token.ML
--- a/src/Pure/Isar/token.ML	Fri Sep 02 19:25:44 2011 +0200
+++ b/src/Pure/Isar/token.ML	Fri Sep 02 20:29:39 2011 +0200
@@ -18,6 +18,7 @@
   val position_of: T -> Position.T
   val end_position_of: T -> Position.T
   val pos_of: T -> string
+  val range: T list -> Position.range
   val eof: T
   val is_eof: T -> bool
   val not_eof: T -> bool
@@ -122,6 +123,13 @@
 
 val pos_of = Position.str_of o position_of;
 
+fun range [] = (Position.none, Position.none)
+  | range toks =
+      let
+        val start_pos = position_of (hd toks);
+        val end_pos = end_position_of (List.last toks);
+      in (start_pos, end_pos) end;
+
 
 (* control tokens *)
 
diff -r 17dbd9d9db38 -r 5bec9c15ef29 src/Pure/Thy/thy_syntax.ML
--- a/src/Pure/Thy/thy_syntax.ML	Fri Sep 02 19:25:44 2011 +0200
+++ b/src/Pure/Thy/thy_syntax.ML	Fri Sep 02 20:29:39 2011 +0200
@@ -16,7 +16,6 @@
   type span
   val span_kind: span -> span_kind
   val span_content: span -> Token.T list
-  val span_range: span -> Position.range
   val span_source: (Token.T, 'a) Source.source -> (span, (Token.T, 'a) Source.source) Source.source
   val parse_spans: Scan.lexicon * Scan.lexicon -> Position.T -> string -> span list
   val present_span: span -> Output.output
@@ -101,15 +100,6 @@
 fun span_kind (Span (k, _)) = k;
 fun span_content (Span (_, toks)) = toks;
 
-fun span_range span =
-  (case span_content span of
-    [] => (Position.none, Position.none)
-  | toks =>
-      let
-        val start_pos = Token.position_of (hd toks);
-        val end_pos = Token.end_position_of (List.last toks);
-      in (start_pos, end_pos) end);
-
 
 (* parse *)