prefer externally provided keywords -- Command.read_thy may degenerate to bootstrap_thy in case of errors;
authorwenzelm
Fri Nov 07 20:06:18 2014 +0100 (2014-11-07)
changeset 58934385a4cc7426f
parent 58933 6585e59aee3e
child 58935 dcad9bad43e7
prefer externally provided keywords -- Command.read_thy may degenerate to bootstrap_thy in case of errors;
tuned message;
src/Pure/Isar/outer_syntax.ML
src/Pure/PIDE/command.ML
src/Pure/PIDE/document.ML
src/Pure/PIDE/resources.ML
     1.1 --- a/src/Pure/Isar/outer_syntax.ML	Fri Nov 07 19:47:05 2014 +0100
     1.2 +++ b/src/Pure/Isar/outer_syntax.ML	Fri Nov 07 20:06:18 2014 +0100
     1.3 @@ -211,8 +211,7 @@
     1.4          SOME (Command {parse, ...}) => Parse.!!! (Parse.tags |-- parse) >> (fn f => f tr0)
     1.5        | NONE =>
     1.6            Scan.succeed
     1.7 -            (tr0 |> Toplevel.imperative (fn () =>
     1.8 -              err_command "Bad parser for outer syntax command " name [pos])))
     1.9 +            (tr0 |> Toplevel.imperative (fn () => err_command "Undefined command " name [pos])))
    1.10      end);
    1.11  
    1.12  val parse_cmt = Parse.$$$ "--" -- Parse.!!! Parse.document_source;
     2.1 --- a/src/Pure/PIDE/command.ML	Fri Nov 07 19:47:05 2014 +0100
     2.2 +++ b/src/Pure/PIDE/command.ML	Fri Nov 07 20:06:18 2014 +0100
     2.3 @@ -9,14 +9,15 @@
     2.4    type blob = (string * (SHA1.digest * string list) option) Exn.result
     2.5    val read_file: Path.T -> Position.T -> Path.T -> Token.file
     2.6    val read_thy: Toplevel.state -> theory
     2.7 -  val read: theory -> Path.T-> (unit -> theory) -> blob list -> Token.T list ->
     2.8 -    Toplevel.transition
     2.9 +  val read: Keyword.keywords -> theory -> Path.T-> (unit -> theory) ->
    2.10 +    blob list -> Token.T list -> Toplevel.transition
    2.11    type eval
    2.12    val eval_eq: eval * eval -> bool
    2.13    val eval_running: eval -> bool
    2.14    val eval_finished: eval -> bool
    2.15    val eval_result_state: eval -> Toplevel.state
    2.16 -  val eval: Path.T -> (unit -> theory) -> blob list -> Token.T list -> eval -> eval
    2.17 +  val eval: Keyword.keywords -> Path.T -> (unit -> theory) ->
    2.18 +    blob list -> Token.T list -> eval -> eval
    2.19    type print
    2.20    val print: bool -> (string * string list) list -> Keyword.keywords -> string ->
    2.21      eval -> print list -> print list option
    2.22 @@ -151,9 +152,8 @@
    2.23  
    2.24  fun read_thy st = Toplevel.theory_of st handle Toplevel.UNDEF => bootstrap_thy;
    2.25  
    2.26 -fun read thy master_dir init blobs span =
    2.27 +fun read keywords thy master_dir init blobs span =
    2.28    let
    2.29 -    val keywords = Thy_Header.get_keywords thy;
    2.30      val command_reports = Outer_Syntax.command_reports thy;
    2.31  
    2.32      val proper_range = Token.range_of (#1 (take_suffix Token.is_improper span));
    2.33 @@ -268,7 +268,7 @@
    2.34  
    2.35  in
    2.36  
    2.37 -fun eval master_dir init blobs span eval0 =
    2.38 +fun eval keywords master_dir init blobs span eval0 =
    2.39    let
    2.40      val exec_id = Document_ID.make ();
    2.41      fun process () =
    2.42 @@ -277,8 +277,8 @@
    2.43          val thy = read_thy (#state eval_state0);
    2.44          val tr =
    2.45            Position.setmp_thread_data (Position.id_only (Document_ID.print exec_id))
    2.46 -            (fn () => read thy master_dir init blobs span |> Toplevel.exec_id exec_id) ();
    2.47 -      in eval_state (Thy_Header.get_keywords thy) span tr eval_state0 end;
    2.48 +            (fn () => read keywords thy master_dir init blobs span |> Toplevel.exec_id exec_id) ();
    2.49 +      in eval_state keywords span tr eval_state0 end;
    2.50    in Eval {exec_id = exec_id, eval_process = memo exec_id process} end;
    2.51  
    2.52  end;
     3.1 --- a/src/Pure/PIDE/document.ML	Fri Nov 07 19:47:05 2014 +0100
     3.2 +++ b/src/Pure/PIDE/document.ML	Fri Nov 07 20:06:18 2014 +0100
     3.3 @@ -544,7 +544,7 @@
     3.4        val span = Lazy.force span0;
     3.5  
     3.6        val eval' =
     3.7 -        Command.eval (master_directory node)
     3.8 +        Command.eval keywords (master_directory node)
     3.9            (fn () => the_default illegal_init init span) blobs span eval;
    3.10        val prints' =
    3.11          perhaps (Command.print command_visible command_overlays keywords command_name eval') [];
     4.1 --- a/src/Pure/PIDE/resources.ML	Fri Nov 07 19:47:05 2014 +0100
     4.2 +++ b/src/Pure/PIDE/resources.ML	Fri Nov 07 20:06:18 2014 +0100
     4.3 @@ -128,7 +128,7 @@
     4.4    let
     4.5      fun prepare_span st span =
     4.6        Command_Span.content span
     4.7 -      |> Command.read (Command.read_thy st) master_dir init []
     4.8 +      |> Command.read keywords (Command.read_thy st) master_dir init []
     4.9        |> (fn tr => Toplevel.put_timing (last_timing tr) tr);
    4.10  
    4.11      fun element_result span_elem (st, _) =