# HG changeset patch
# User wenzelm
# Date 1331829626 -3600
# Node ID 26007caf6e9c5f8136a4d05c1d6788282826a2eb
# Parent  9fc22eb6408c455a102c6cfe2260bb8aaa5bcc0e
declare keywords as side-effect of header edit;
parse_command span is now lazy instead of future, to happen synchronously after header edit in new_exec (before execution);

diff -r 9fc22eb6408c -r 26007caf6e9c src/Pure/Isar/keyword.ML
--- a/src/Pure/Isar/keyword.ML	Thu Mar 15 14:39:42 2012 +0100
+++ b/src/Pure/Isar/keyword.ML	Thu Mar 15 17:40:26 2012 +0100
@@ -48,6 +48,7 @@
   val status: unit -> unit
   val keyword: string -> unit
   val command: string -> T -> unit
+  val declare: string * (string * string list) option -> unit
   val is_diag: string -> bool
   val is_control: string -> bool
   val is_regular: string -> bool
@@ -214,6 +215,9 @@
   change_commands (Symtab.update (name, kind));
   command_status (name, kind));
 
+fun declare (name, NONE) = keyword name
+  | declare (name, SOME kind) = command name (make kind);
+
 
 (* command categories *)
 
diff -r 9fc22eb6408c -r 26007caf6e9c src/Pure/PIDE/document.ML
--- a/src/Pure/PIDE/document.ML	Thu Mar 15 14:39:42 2012 +0100
+++ b/src/Pure/PIDE/document.ML	Thu Mar 15 17:40:26 2012 +0100
@@ -213,16 +213,20 @@
     | Header header =>
         let
           val imports = (case header of Exn.Res (_, {imports, ...}) => imports | _ => []);
+          val keywords = (case header of Exn.Res (_, {keywords, ...}) => keywords | _ => []);
+          val header' =
+            (List.app Keyword.declare keywords; header)
+              handle exn as ERROR _ => Exn.Exn exn;
           val nodes1 = nodes
             |> default_node name
             |> fold default_node imports;
           val nodes2 = nodes1
             |> Graph.Keys.fold
                 (fn dep => Graph.del_edge (dep, name)) (Graph.imm_preds nodes1 name);
-          val (header', nodes3) =
-            (header, Graph.add_deps_acyclic (name, imports) nodes2)
+          val (header'', nodes3) =
+            (header', Graph.add_deps_acyclic (name, imports) nodes2)
               handle Graph.CYCLES cs => (Exn.Exn (ERROR (cat_lines (map cycle_msg cs))), nodes2);
-        in Graph.map_node name (set_header header') nodes3 end
+        in Graph.map_node name (set_header header'') nodes3 end
         |> touch_node name
     | Perspective perspective =>
         update_node name (set_perspective perspective) nodes);
@@ -240,7 +244,7 @@
 
 abstype state = State of
  {versions: version Inttab.table,  (*version_id -> document content*)
-  commands: (string * Token.T list future) Inttab.table,  (*command_id -> name * span*)
+  commands: (string * Token.T list lazy) Inttab.table,  (*command_id -> name * span*)
   execution: version_id * Future.group}  (*current execution process*)
 with
 
@@ -284,13 +288,9 @@
 fun define_command (id: command_id) name text =
   map_state (fn (versions, commands, execution) =>
     let
-      val future =
-        (singleton o Future.forks)
-          {name = "Document.define_command", group = SOME (Future.new_group NONE),
-            deps = [], pri = ~1, interrupts = false}
-          (fn () => parse_command (print_id id) text);
+      val span = Lazy.lazy (fn () => parse_command (print_id id) text);
       val commands' =
-        Inttab.update_new (id, (name, future)) commands
+        Inttab.update_new (id, (name, span)) commands
           handle Inttab.DUP dup => err_dup "command" dup;
     in (versions, commands', execution) end);
 
@@ -412,7 +412,7 @@
   if bad_init andalso is_none init then NONE
   else
     let
-      val (name, span) = the_command state command_id' ||> Future.join;
+      val (name, span) = the_command state command_id' ||> Lazy.force;
       val (modify_init, init') =
         if Keyword.is_theory_begin name then
           (Toplevel.modify_init (the_default illegal_init init), NONE)