# HG changeset patch
# User wenzelm
# Date 1344701141 -7200
# Node ID 2ea997196d048858035dcdb151634a8c57a1bc7c
# Parent  85eeb06ec1c442ecdbf56631b90afdf160ce4910
clarified Command.range vs. Command.proper_range according to Scala version, which is potentially relevant for command status markup;

diff -r 85eeb06ec1c4 -r 2ea997196d04 src/Pure/Isar/outer_syntax.ML
--- a/src/Pure/Isar/outer_syntax.ML	Sat Aug 11 17:43:00 2012 +0200
+++ b/src/Pure/Isar/outer_syntax.ML	Sat Aug 11 18:05:41 2012 +0200
@@ -273,11 +273,11 @@
   let
     val commands = lookup_commands outer_syntax;
 
-    val range_pos = Position.set_range (Token.range toks);
+    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 => range_pos);
+      | NONE => proper_range);
 
     fun command_reports tok =
       if Token.is_command tok then
@@ -298,9 +298,9 @@
           if Keyword.is_control (Toplevel.name_of tr) then
             (Toplevel.malformed pos "Illegal control command", true)
           else (tr, true)
-      | [] => (Toplevel.ignored range_pos, false)
-      | _ => (Toplevel.malformed range_pos "Exactly one command expected", true))
-      handle ERROR msg => (Toplevel.malformed range_pos msg, true)
+      | [] => (Toplevel.ignored (Position.set_range (Command.range toks)), false)
+      | _ => (Toplevel.malformed proper_range "Exactly one command expected", true))
+      handle ERROR msg => (Toplevel.malformed proper_range msg, true)
   end;
 
 fun read_element outer_syntax init {head, proof, proper_proof} =
diff -r 85eeb06ec1c4 -r 2ea997196d04 src/Pure/Isar/token.ML
--- a/src/Pure/Isar/token.ML	Sat Aug 11 17:43:00 2012 +0200
+++ b/src/Pure/Isar/token.ML	Sat Aug 11 18:05:41 2012 +0200
@@ -18,7 +18,6 @@
   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
@@ -35,6 +34,7 @@
   val is_begin_ignore: T -> bool
   val is_end_ignore: T -> bool
   val is_error: T -> bool
+  val is_space: T -> bool
   val is_blank: T -> bool
   val is_newline: T -> bool
   val source_of: T -> string
@@ -125,13 +125,6 @@
 
 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 *)
 
@@ -185,6 +178,9 @@
 
 (* blanks and newlines -- space tokens obey lines *)
 
+fun is_space (Token (_, (Space, _), _)) = true
+  | is_space _ = false;
+
 fun is_blank (Token (_, (Space, x), _)) = not (String.isSuffix "\n" x)
   | is_blank _ = false;
 
@@ -315,11 +311,11 @@
 
 (* scan space *)
 
-fun is_space s = Symbol.is_blank s andalso s <> "\n";
+fun space_symbol (s, _) = Symbol.is_blank s andalso s <> "\n";
 
 val scan_space =
-  Scan.many1 (is_space o Symbol_Pos.symbol) @@@ Scan.optional ($$$ "\n") [] ||
-  Scan.many (is_space o Symbol_Pos.symbol) @@@ $$$ "\n";
+  Scan.many1 space_symbol @@@ Scan.optional ($$$ "\n") [] ||
+  Scan.many space_symbol @@@ $$$ "\n";
 
 
 (* scan comment *)
diff -r 85eeb06ec1c4 -r 2ea997196d04 src/Pure/PIDE/command.ML
--- a/src/Pure/PIDE/command.ML	Sat Aug 11 17:43:00 2012 +0200
+++ b/src/Pure/PIDE/command.ML	Sat Aug 11 18:05:41 2012 +0200
@@ -6,6 +6,8 @@
 
 signature COMMAND =
 sig
+  val range: Token.T list -> Position.range
+  val proper_range: Token.T list -> Position.range
   type 'a memo
   val memo: (unit -> 'a) -> 'a memo
   val memo_value: 'a -> 'a memo
@@ -17,6 +19,18 @@
 structure Command: COMMAND =
 struct
 
+(* span range *)
+
+fun range [] = (Position.none, Position.none)
+  | range 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;
+
+val proper_range = range o #1 o take_suffix Token.is_space;
+
+
 (* memo results *)
 
 datatype 'a expr =
diff -r 85eeb06ec1c4 -r 2ea997196d04 src/Pure/ROOT.ML
--- a/src/Pure/ROOT.ML	Sat Aug 11 17:43:00 2012 +0200
+++ b/src/Pure/ROOT.ML	Sat Aug 11 18:05:41 2012 +0200
@@ -247,11 +247,11 @@
 use "Thy/term_style.ML";
 use "Thy/thy_output.ML";
 use "Thy/thy_syntax.ML";
+use "PIDE/command.ML";
 use "Isar/outer_syntax.ML";
 use "Thy/present.ML";
 use "Thy/thy_load.ML";
 use "Thy/thy_info.ML";
-use "PIDE/command.ML";
 use "PIDE/document.ML";
 use "Thy/rail.ML";