src/Pure/PIDE/document.ML
changeset 60880 fa958e24ff24
parent 60198 8483c2883c8c
child 60937 51425cbe8ce9
     1.1 --- a/src/Pure/PIDE/document.ML	Mon Aug 10 19:17:49 2015 +0200
     1.2 +++ b/src/Pure/PIDE/document.ML	Mon Aug 10 20:22:49 2015 +0200
     1.3 @@ -21,6 +21,7 @@
     1.4    type blob_digest = (string * string option) Exn.result
     1.5    val define_command: Document_ID.command -> string -> blob_digest list -> int ->
     1.6      ((int * int) * string) list -> state -> state
     1.7 +  val command_exec: state -> string -> Document_ID.command -> Command.exec option
     1.8    val remove_versions: Document_ID.version list -> state -> state
     1.9    val start_execution: state -> state
    1.10    val update: Document_ID.version -> Document_ID.version -> edit list -> state ->
    1.11 @@ -406,6 +407,12 @@
    1.12  
    1.13  val the_command_name = #1 oo the_command;
    1.14  
    1.15 +fun command_exec state node_name command_id =
    1.16 +  let
    1.17 +    val State {execution = {version_id, ...}, ...} = state;
    1.18 +    val node = get_node (nodes_of (the_version state version_id)) node_name;
    1.19 +  in the_entry node command_id end;
    1.20 +
    1.21  end;
    1.22  
    1.23