src/Pure/PIDE/document.ML
changeset 59085 08a6901eb035
parent 59083 88b0b1f28adc
child 59086 94b2690ad494
     1.1 --- a/src/Pure/PIDE/document.ML	Wed Dec 03 15:22:27 2014 +0100
     1.2 +++ b/src/Pure/PIDE/document.ML	Wed Dec 03 20:45:20 2014 +0100
     1.3 @@ -20,8 +20,8 @@
     1.4    val init_state: state
     1.5    val define_blob: string -> string -> state -> state
     1.6    type blob_digest = (string * string option) Exn.result
     1.7 -  val define_command: Document_ID.command -> string -> blob_digest list -> string ->
     1.8 -    state -> state
     1.9 +  val define_command: Document_ID.command -> string -> blob_digest list ->
    1.10 +    ((int * int) * string) list -> state -> state
    1.11    val remove_versions: Document_ID.version list -> state -> state
    1.12    val start_execution: state -> state
    1.13    val update: Document_ID.version -> Document_ID.version -> edit list -> state ->
    1.14 @@ -326,14 +326,14 @@
    1.15  
    1.16  (* commands *)
    1.17  
    1.18 -fun define_command command_id name command_blobs text =
    1.19 +fun define_command command_id name command_blobs toks =
    1.20    map_state (fn (versions, blobs, commands, execution) =>
    1.21      let
    1.22        val id = Document_ID.print command_id;
    1.23        val span =
    1.24          Lazy.lazy (fn () =>
    1.25            Position.setmp_thread_data (Position.id_only id)
    1.26 -            (fn () => Token.explode (get_keywords ()) (Position.id id) text) ());
    1.27 +            (fn () => #1 (fold_map Token.make toks (Position.id id))) ());
    1.28        val _ =
    1.29          Position.setmp_thread_data (Position.id_only id)
    1.30            (fn () => Output.status (Markup.markup_only Markup.accepted)) ();