# HG changeset patch
# User wenzelm
# Date 1429189203 -7200
# Node ID 35f626b1142229f7df674a1007ce26d26889ad7e
# Parent  96a4765ba7d10abfc93a29dac9f747d282b9de78
more explicit bootstrap_thy;
clarified error;

diff -r 96a4765ba7d1 -r 35f626b11422 src/Pure/Isar/outer_syntax.ML
--- a/src/Pure/Isar/outer_syntax.ML	Thu Apr 16 14:18:32 2015 +0200
+++ b/src/Pure/Isar/outer_syntax.ML	Thu Apr 16 15:00:03 2015 +0200
@@ -19,6 +19,7 @@
     (bool -> local_theory -> Proof.state) parser -> unit
   val local_theory_to_proof: command_keyword -> string ->
     (local_theory -> Proof.state) parser -> unit
+  val bootstrap: bool Config.T
   val parse: theory -> Position.T -> string -> Toplevel.transition list
   val parse_tokens: theory -> Token.T list -> Toplevel.transition list
   val parse_spans: Token.T list -> Command_Span.span list
@@ -160,6 +161,9 @@
 
 (* parse commands *)
 
+val bootstrap =
+  Config.bool (Config.declare ("Outer_Syntax.bootstrap", @{here}) (K (Config.Bool true)));
+
 local
 
 val before_command =
@@ -177,7 +181,14 @@
       | SOME (Command {command_parser = Limited_Parser parse, ...}) =>
           before_command :|-- (fn limited =>
             Parse.!!! (command_tags |-- parse limited)) >> (fn f => f tr0)
-      | NONE => Scan.fail_with (fn _ => fn _ => err_command "Undefined command " name [pos]))
+      | NONE =>
+          Scan.fail_with (fn _ => fn _ =>
+            let
+              val msg =
+                if Config.get_global thy bootstrap
+                then "missing theory context for command "
+                else "undefined command ";
+            in msg ^ quote (Markup.markup Markup.keyword1 name) end))
     end);
 
 val parse_cmt = Parse.$$$ "--" -- Parse.!!! Parse.document_source;
diff -r 96a4765ba7d1 -r 35f626b11422 src/Pure/PIDE/command.ML
--- a/src/Pure/PIDE/command.ML	Thu Apr 16 14:18:32 2015 +0200
+++ b/src/Pure/PIDE/command.ML	Thu Apr 16 15:00:03 2015 +0200
@@ -109,11 +109,10 @@
       | NONE => toks)
   | _ => toks);
 
-val bootstrap_thy = ML_Context.the_global_context ();
-
 in
 
-fun read_thy st = Toplevel.theory_of st handle Toplevel.UNDEF => bootstrap_thy;
+fun read_thy st = Toplevel.theory_of st
+  handle Toplevel.UNDEF => Pure_Syn.bootstrap_thy;
 
 fun read keywords thy master_dir init blobs_info span =
   let
diff -r 96a4765ba7d1 -r 35f626b11422 src/Pure/pure_syn.ML
--- a/src/Pure/pure_syn.ML	Thu Apr 16 14:18:32 2015 +0200
+++ b/src/Pure/pure_syn.ML	Thu Apr 16 15:00:03 2015 +0200
@@ -4,7 +4,12 @@
 Outer syntax for bootstrapping Isabelle/Pure.
 *)
 
-structure Pure_Syn: sig end =
+signature PURE_SYN =
+sig
+  val bootstrap_thy: theory
+end;
+
+structure Pure_Syn: PURE_SYN =
 struct
 
 val _ =
@@ -44,5 +49,9 @@
     (Thy_Header.args >>
       (fn _ => Toplevel.init_theory (fn () => error "Missing theory initialization")));
 
+
+val bootstrap_thy = ML_Context.the_global_context ();
+
+val _ = Theory.setup (Config.put_global Outer_Syntax.bootstrap false);
+
 end;
-