clarified define_command: send tokens more directly, without requiring keywords in ML;

--- a/src/Pure/General/position.ML	Wed Dec 03 15:22:27 2014 +0100
+++ b/src/Pure/General/position.ML	Wed Dec 03 20:45:20 2014 +0100
@@ -14,6 +14,7 @@
   val end_offset_of: T -> int option
   val file_of: T -> string option
   val advance: Symbol.symbol -> T -> T
+  val advance_offset: int -> T -> T
   val distance_of: T -> T -> int
   val none: T
   val start: T
@@ -101,6 +102,11 @@
 fun advance sym (pos as (Pos (count, props))) =
   if invalid_count count then pos else Pos (advance_count sym count, props);
 
+fun advance_offset offset (pos as (Pos (count as (i, j, k), props))) =
+  if invalid_count count then pos
+  else if valid i then raise Fail "Illegal line position"
+  else Pos ((i, if_valid j (j + offset), k), props);
+
 
 (* distance of adjacent positions *)
 

--- a/src/Pure/Isar/token.ML	Wed Dec 03 15:22:27 2014 +0100
+++ b/src/Pure/Isar/token.ML	Wed Dec 03 20:45:20 2014 +0100
@@ -90,6 +90,7 @@
     Position.T -> (Symbol.symbol, 'a) Source.source -> (T,
       (Symbol_Pos.T, Position.T * (Symbol.symbol, 'a) Source.source) Source.source) Source.source
   val explode: Keyword.keywords -> Position.T -> string -> T list
+  val make: (int * int) * string -> Position.T -> T * Position.T
   type 'a parser = T list -> 'a * T list
   type 'a context_parser = Context.generic * T list -> 'a * (Context.generic * T list)
   val read_no_commands: Keyword.keywords -> 'a parser -> Symbol_Pos.T list -> 'a list
@@ -135,6 +136,10 @@
   | Error _ => "bad input"
   | EOF => "end-of-input";
 
+val immediate_kinds =
+  Vector.fromList
+    [Command, Keyword, Ident, Long_Ident, Sym_Ident, Var, Type_Ident, Type_Var, Nat, Float, Space];
+
 val delimited_kind = member (op =) [String, Alt_String, Verbatim, Cartouche, Comment];
 
 
@@ -591,6 +596,22 @@
   Source.exhaust;
 
 
+(* make *)
+
+fun make ((k, n), s) pos =
+  let
+    val pos' = Position.advance_offset n pos;
+    val range = Position.range pos pos';
+    val tok =
+      if k < Vector.length immediate_kinds then
+        Token ((s, range), (Vector.sub (immediate_kinds, k), s), Slot)
+      else
+        (case explode Keyword.empty_keywords pos s of
+          [tok] => tok
+        | _ => Token ((s, range), (Error (err_prefix ^ "exactly one token expected"), s), Slot))
+  in (tok, pos') end;
+
+
 
 (** parsers **)
 

--- a/src/Pure/PIDE/document.ML	Wed Dec 03 15:22:27 2014 +0100
+++ b/src/Pure/PIDE/document.ML	Wed Dec 03 20:45:20 2014 +0100
@@ -20,8 +20,8 @@
   val init_state: state
   val define_blob: string -> string -> state -> state
   type blob_digest = (string * string option) Exn.result
-  val define_command: Document_ID.command -> string -> blob_digest list -> string ->
-    state -> state
+  val define_command: Document_ID.command -> string -> blob_digest list ->
+    ((int * int) * string) list -> state -> state
   val remove_versions: Document_ID.version list -> state -> state
   val start_execution: state -> state
   val update: Document_ID.version -> Document_ID.version -> edit list -> state ->
@@ -326,14 +326,14 @@
 
 (* commands *)
 
-fun define_command command_id name command_blobs text =
+fun define_command command_id name command_blobs toks =
   map_state (fn (versions, blobs, commands, execution) =>
     let
       val id = Document_ID.print command_id;
       val span =
         Lazy.lazy (fn () =>
           Position.setmp_thread_data (Position.id_only id)
-            (fn () => Token.explode (get_keywords ()) (Position.id id) text) ());
+            (fn () => #1 (fold_map Token.make toks (Position.id id))) ());
       val _ =
         Position.setmp_thread_data (Position.id_only id)
           (fn () => Output.status (Markup.markup_only Markup.accepted)) ();

--- a/src/Pure/PIDE/protocol.ML	Wed Dec 03 15:22:27 2014 +0100
+++ b/src/Pure/PIDE/protocol.ML	Wed Dec 03 20:45:20 2014 +0100
@@ -32,7 +32,7 @@
 
 val _ =
   Isabelle_Process.protocol_command "Document.define_command"
-    (fn [id, name, blobs_yxml, text] =>
+    (fn id :: name :: blobs_yxml :: toks_yxml :: sources =>
       let
         val blobs =
           YXML.parse_body blobs_yxml |>
@@ -41,8 +41,10 @@
                [fn ([], a) => Exn.Res (pair string (option string) a),
                 fn ([], a) => Exn.Exn (ERROR (string a))])
             end;
+        val toks =
+          (YXML.parse_body toks_yxml |> let open XML.Decode in list (pair int int) end) ~~ sources;
       in
-        Document.change_state (Document.define_command (Document_ID.parse id) name blobs text)
+        Document.change_state (Document.define_command (Document_ID.parse id) name blobs toks)
       end);
 
 val _ =

--- a/src/Pure/PIDE/protocol.scala	Wed Dec 03 15:22:27 2014 +0100
+++ b/src/Pure/PIDE/protocol.scala	Wed Dec 03 20:45:20 2014 +0100
@@ -392,10 +392,21 @@
           { case Exn.Res((a, b)) =>
               (Nil, pair(string, option(string))((a.node, b.map(p => p._1.toString)))) },
           { case Exn.Exn(e) => (Nil, string(Exn.message(e))) }))
+
       YXML.string_of_body(list(encode_blob)(command.blobs))
     }
+
+    val toks = command.span.content
+    val toks_yxml =
+    { import XML.Encode._
+      val encode_tok: T[Token] =
+        (tok => pair(int, int)((tok.kind.id, Symbol.iterator(tok.source).length)))
+      YXML.string_of_body(list(encode_tok)(toks))
+    }
+
     protocol_command("Document.define_command",
-      Document_ID(command.id), encode(command.name), blobs_yxml, encode(command.source))
+      (Document_ID(command.id) :: encode(command.name) :: blobs_yxml :: toks_yxml ::
+        toks.map(tok => encode(tok.source))): _*)
   }