src/Pure/PIDE/document.ML

   type edit = string * node_edit
   type state
   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 -> int ->
-    ((int * int) * string) list -> state -> state
+  type command =
+   {command_id: Document_ID.command,
+    name: string,
+    blobs_digests: blob_digest list,
+    blobs_index: int,
+    tokens: ((int * int) * string) list}
+  val define_command: command -> state -> state
   val command_exec: state -> string -> Document_ID.command -> Command.exec option
   val remove_versions: Document_ID.version list -> state -> state
   val start_execution: state -> state
   val update: Document_ID.version -> Document_ID.version -> edit list -> string list -> state ->
     string list * Document_ID.exec list * (Document_ID.command * Document_ID.exec list) list * state

   (case blob_digest of Exn.Res (file_node, _) => [(pos, Markup.path file_node)] | _ => []);
 
 
 (* commands *)
 
-fun define_command command_id name blobs_digests blobs_index toks =
+type command =
+  {command_id: Document_ID.command,
+   name: string,
+   blobs_digests: blob_digest list,
+   blobs_index: int,
+   tokens: ((int * int) * string) list};
+
+fun define_command {command_id, name, blobs_digests, blobs_index, tokens} =
   map_state (fn (versions, blobs, commands, execution) =>
     let
       val id = Document_ID.print command_id;
       val span =
         Lazy.lazy_name "Document.define_command" (fn () =>
           Position.setmp_thread_data (Position.id_only id)
             (fn () =>
               let
-                val (tokens, _) = fold_map Token.make toks (Position.id id);
+                val (tokens, _) = fold_map Token.make tokens (Position.id id);
                 val _ =
                   if blobs_index < 0
                   then (*inlined errors*)
                     map_filter Exn.get_exn blobs_digests
                     |> List.app (Output.error_message o Runtime.exn_message)