1.1 --- a/src/Pure/Isar/keyword.ML	Thu Mar 15 14:39:42 2012 +0100
     1.2 +++ b/src/Pure/Isar/keyword.ML	Thu Mar 15 17:40:26 2012 +0100
     1.3 @@ -48,6 +48,7 @@
     1.4    val status: unit -> unit
     1.5    val keyword: string -> unit
     1.6    val command: string -> T -> unit
     1.7 +  val declare: string * (string * string list) option -> unit
     1.8    val is_diag: string -> bool
     1.9    val is_control: string -> bool
    1.10    val is_regular: string -> bool
    1.11 @@ -214,6 +215,9 @@
    1.12    change_commands (Symtab.update (name, kind));
    1.13    command_status (name, kind));
    1.14  
    1.15 +fun declare (name, NONE) = keyword name
    1.16 +  | declare (name, SOME kind) = command name (make kind);
    1.17 +
    1.18  
    1.19  (* command categories *)
    1.20  

     2.1 --- a/src/Pure/PIDE/document.ML	Thu Mar 15 14:39:42 2012 +0100
     2.2 +++ b/src/Pure/PIDE/document.ML	Thu Mar 15 17:40:26 2012 +0100
     2.3 @@ -213,16 +213,20 @@
     2.4      | Header header =>
     2.5          let
     2.6            val imports = (case header of Exn.Res (_, {imports, ...}) => imports | _ => []);
     2.7 +          val keywords = (case header of Exn.Res (_, {keywords, ...}) => keywords | _ => []);
     2.8 +          val header' =
     2.9 +            (List.app Keyword.declare keywords; header)
    2.10 +              handle exn as ERROR _ => Exn.Exn exn;
    2.11            val nodes1 = nodes
    2.12              |> default_node name
    2.13              |> fold default_node imports;
    2.14            val nodes2 = nodes1
    2.15              |> Graph.Keys.fold
    2.16                  (fn dep => Graph.del_edge (dep, name)) (Graph.imm_preds nodes1 name);
    2.17 -          val (header', nodes3) =
    2.18 -            (header, Graph.add_deps_acyclic (name, imports) nodes2)
    2.19 +          val (header'', nodes3) =
    2.20 +            (header', Graph.add_deps_acyclic (name, imports) nodes2)
    2.21                handle Graph.CYCLES cs => (Exn.Exn (ERROR (cat_lines (map cycle_msg cs))), nodes2);
    2.22 -        in Graph.map_node name (set_header header') nodes3 end
    2.23 +        in Graph.map_node name (set_header header'') nodes3 end
    2.24          |> touch_node name
    2.25      | Perspective perspective =>
    2.26          update_node name (set_perspective perspective) nodes);
    2.27 @@ -240,7 +244,7 @@
    2.28  
    2.29  abstype state = State of
    2.30   {versions: version Inttab.table,  (*version_id -> document content*)
    2.31 -  commands: (string * Token.T list future) Inttab.table,  (*command_id -> name * span*)
    2.32 +  commands: (string * Token.T list lazy) Inttab.table,  (*command_id -> name * span*)
    2.33    execution: version_id * Future.group}  (*current execution process*)
    2.34  with
    2.35  
    2.36 @@ -284,13 +288,9 @@
    2.37  fun define_command (id: command_id) name text =
    2.38    map_state (fn (versions, commands, execution) =>
    2.39      let
    2.40 -      val future =
    2.41 -        (singleton o Future.forks)
    2.42 -          {name = "Document.define_command", group = SOME (Future.new_group NONE),
    2.43 -            deps = [], pri = ~1, interrupts = false}
    2.44 -          (fn () => parse_command (print_id id) text);
    2.45 +      val span = Lazy.lazy (fn () => parse_command (print_id id) text);
    2.46        val commands' =
    2.47 -        Inttab.update_new (id, (name, future)) commands
    2.48 +        Inttab.update_new (id, (name, span)) commands
    2.49            handle Inttab.DUP dup => err_dup "command" dup;
    2.50      in (versions, commands', execution) end);
    2.51  
    2.52 @@ -412,7 +412,7 @@
    2.53    if bad_init andalso is_none init then NONE
    2.54    else
    2.55      let
    2.56 -      val (name, span) = the_command state command_id' ||> Future.join;
    2.57 +      val (name, span) = the_command state command_id' ||> Lazy.force;
    2.58        val (modify_init, init') =
    2.59          if Keyword.is_theory_begin name then
    2.60            (Toplevel.modify_init (the_default illegal_init init), NONE)