# HG changeset patch
# User wenzelm
# Date 1415387178 -3600
# Node ID 385a4cc7426fc4e7ad838e391fb966a5c2d878fd
# Parent  6585e59aee3e54f704a8b388e2fe9a846213bdaa
prefer externally provided keywords -- Command.read_thy may degenerate to bootstrap_thy in case of errors;
tuned message;

diff -r 6585e59aee3e -r 385a4cc7426f src/Pure/Isar/outer_syntax.ML
--- a/src/Pure/Isar/outer_syntax.ML	Fri Nov 07 19:47:05 2014 +0100
+++ b/src/Pure/Isar/outer_syntax.ML	Fri Nov 07 20:06:18 2014 +0100
@@ -211,8 +211,7 @@
         SOME (Command {parse, ...}) => Parse.!!! (Parse.tags |-- parse) >> (fn f => f tr0)
       | NONE =>
           Scan.succeed
-            (tr0 |> Toplevel.imperative (fn () =>
-              err_command "Bad parser for outer syntax command " name [pos])))
+            (tr0 |> Toplevel.imperative (fn () => err_command "Undefined command " name [pos])))
     end);
 
 val parse_cmt = Parse.$$$ "--" -- Parse.!!! Parse.document_source;
diff -r 6585e59aee3e -r 385a4cc7426f src/Pure/PIDE/command.ML
--- a/src/Pure/PIDE/command.ML	Fri Nov 07 19:47:05 2014 +0100
+++ b/src/Pure/PIDE/command.ML	Fri Nov 07 20:06:18 2014 +0100
@@ -9,14 +9,15 @@
   type blob = (string * (SHA1.digest * string list) option) Exn.result
   val read_file: Path.T -> Position.T -> Path.T -> Token.file
   val read_thy: Toplevel.state -> theory
-  val read: theory -> Path.T-> (unit -> theory) -> blob list -> Token.T list ->
-    Toplevel.transition
+  val read: Keyword.keywords -> theory -> Path.T-> (unit -> theory) ->
+    blob list -> Token.T list -> Toplevel.transition
   type eval
   val eval_eq: eval * eval -> bool
   val eval_running: eval -> bool
   val eval_finished: eval -> bool
   val eval_result_state: eval -> Toplevel.state
-  val eval: Path.T -> (unit -> theory) -> blob list -> Token.T list -> eval -> eval
+  val eval: Keyword.keywords -> Path.T -> (unit -> theory) ->
+    blob list -> Token.T list -> eval -> eval
   type print
   val print: bool -> (string * string list) list -> Keyword.keywords -> string ->
     eval -> print list -> print list option
@@ -151,9 +152,8 @@
 
 fun read_thy st = Toplevel.theory_of st handle Toplevel.UNDEF => bootstrap_thy;
 
-fun read thy master_dir init blobs span =
+fun read keywords thy master_dir init blobs span =
   let
-    val keywords = Thy_Header.get_keywords thy;
     val command_reports = Outer_Syntax.command_reports thy;
 
     val proper_range = Token.range_of (#1 (take_suffix Token.is_improper span));
@@ -268,7 +268,7 @@
 
 in
 
-fun eval master_dir init blobs span eval0 =
+fun eval keywords master_dir init blobs span eval0 =
   let
     val exec_id = Document_ID.make ();
     fun process () =
@@ -277,8 +277,8 @@
         val thy = read_thy (#state eval_state0);
         val tr =
           Position.setmp_thread_data (Position.id_only (Document_ID.print exec_id))
-            (fn () => read thy master_dir init blobs span |> Toplevel.exec_id exec_id) ();
-      in eval_state (Thy_Header.get_keywords thy) span tr eval_state0 end;
+            (fn () => read keywords thy master_dir init blobs span |> Toplevel.exec_id exec_id) ();
+      in eval_state keywords span tr eval_state0 end;
   in Eval {exec_id = exec_id, eval_process = memo exec_id process} end;
 
 end;
diff -r 6585e59aee3e -r 385a4cc7426f src/Pure/PIDE/document.ML
--- a/src/Pure/PIDE/document.ML	Fri Nov 07 19:47:05 2014 +0100
+++ b/src/Pure/PIDE/document.ML	Fri Nov 07 20:06:18 2014 +0100
@@ -544,7 +544,7 @@
       val span = Lazy.force span0;
 
       val eval' =
-        Command.eval (master_directory node)
+        Command.eval keywords (master_directory node)
           (fn () => the_default illegal_init init span) blobs span eval;
       val prints' =
         perhaps (Command.print command_visible command_overlays keywords command_name eval') [];
diff -r 6585e59aee3e -r 385a4cc7426f src/Pure/PIDE/resources.ML
--- a/src/Pure/PIDE/resources.ML	Fri Nov 07 19:47:05 2014 +0100
+++ b/src/Pure/PIDE/resources.ML	Fri Nov 07 20:06:18 2014 +0100
@@ -128,7 +128,7 @@
   let
     fun prepare_span st span =
       Command_Span.content span
-      |> Command.read (Command.read_thy st) master_dir init []
+      |> Command.read keywords (Command.read_thy st) master_dir init []
       |> (fn tr => Toplevel.put_timing (last_timing tr) tr);
 
     fun element_result span_elem (st, _) =