more official command specifications, including source position;
authorwenzelm
Thu Aug 02 12:36:54 2012 +0200 (2012-08-02)
changeset 4864691281e9472d8
parent 48645 33f00ce23e63
child 48647 a5144c4c26a2
more official command specifications, including source position;
src/Pure/Isar/isar_syn.ML
src/Pure/Isar/keyword.ML
src/Pure/Isar/outer_syntax.ML
src/Pure/ML/ml_antiquote.ML
src/Pure/Proof/extraction.ML
src/Pure/ProofGeneral/proof_general_emacs.ML
src/Pure/ProofGeneral/proof_general_pgip.ML
src/Pure/Pure.thy
src/Pure/ROOT
src/Pure/ROOT.ML
src/Pure/System/isar.ML
src/Pure/System/session.ML
src/Pure/Tools/find_consts.ML
src/Pure/Tools/find_theorems.ML
src/Pure/pure_setup.ML
     1.1 --- a/src/Pure/Isar/isar_syn.ML	Thu Aug 02 11:32:23 2012 +0200
     1.2 +++ b/src/Pure/Isar/isar_syn.ML	Thu Aug 02 12:36:54 2012 +0200
     1.3 @@ -989,6 +989,75 @@
     1.4          (Context.set_thread_data (try Toplevel.generic_theory_of state);
     1.5            raise Runtime.TERMINATE))));
     1.6  
     1.7 +val _ =
     1.8 +  Outer_Syntax.improper_command @{command_spec "welcome"} "print welcome message"
     1.9 +    (Scan.succeed (Toplevel.no_timing o Toplevel.imperative (writeln o Session.welcome)));
    1.10 +
    1.11 +
    1.12 +
    1.13 +(** raw Isar read-eval-print loop **)
    1.14 +
    1.15 +val _ =
    1.16 +  Outer_Syntax.improper_command @{command_spec "init_toplevel"} "init toplevel point-of-interest"
    1.17 +    (Scan.succeed (Toplevel.no_timing o Toplevel.imperative Isar.init));
    1.18 +
    1.19 +val _ =
    1.20 +  Outer_Syntax.improper_command @{command_spec "linear_undo"} "undo commands"
    1.21 +    (Scan.optional Parse.nat 1 >>
    1.22 +      (fn n => Toplevel.no_timing o Toplevel.imperative (fn () => Isar.linear_undo n)));
    1.23 +
    1.24 +val _ =
    1.25 +  Outer_Syntax.improper_command @{command_spec "undo"} "undo commands (skipping closed proofs)"
    1.26 +    (Scan.optional Parse.nat 1 >>
    1.27 +      (fn n => Toplevel.no_timing o Toplevel.imperative (fn () => Isar.undo n)));
    1.28 +
    1.29 +val _ =
    1.30 +  Outer_Syntax.improper_command @{command_spec "undos_proof"}
    1.31 +    "undo commands (skipping closed proofs)"
    1.32 +    (Scan.optional Parse.nat 1 >> (fn n => Toplevel.no_timing o
    1.33 +      Toplevel.keep (fn state =>
    1.34 +        if Toplevel.is_proof state then (Isar.undo n; Isar.print ()) else raise Toplevel.UNDEF)));
    1.35 +
    1.36 +val _ =
    1.37 +  Outer_Syntax.improper_command @{command_spec "cannot_undo"}
    1.38 +    "partial undo -- Proof General legacy"
    1.39 +    (Parse.name >>
    1.40 +      (fn "end" => Toplevel.no_timing o Toplevel.imperative (fn () => Isar.undo 1)
    1.41 +        | txt => Toplevel.imperative (fn () => error ("Cannot undo " ^ quote txt))));
    1.42 +
    1.43 +val _ =
    1.44 +  Outer_Syntax.improper_command @{command_spec "kill"}
    1.45 +    "kill partial proof or theory development"
    1.46 +    (Scan.succeed (Toplevel.no_timing o Toplevel.imperative Isar.kill));
    1.47 +
    1.48 +
    1.49 +
    1.50 +(** extraction of programs from proofs **)
    1.51 +
    1.52 +val parse_vars = Scan.optional (Parse.$$$ "(" |-- Parse.list1 Parse.name --| Parse.$$$ ")") [];
    1.53 +
    1.54 +val _ =
    1.55 +  Outer_Syntax.command @{command_spec "realizers"}
    1.56 +    "specify realizers for primitive axioms / theorems, together with correctness proof"
    1.57 +    (Scan.repeat1 (Parse.xname -- parse_vars --| Parse.$$$ ":" -- Parse.string -- Parse.string) >>
    1.58 +     (fn xs => Toplevel.theory (fn thy => Extraction.add_realizers
    1.59 +       (map (fn (((a, vs), s1), s2) => (Global_Theory.get_thm thy a, (vs, s1, s2))) xs) thy)));
    1.60 +
    1.61 +val _ =
    1.62 +  Outer_Syntax.command @{command_spec "realizability"}
    1.63 +    "add equations characterizing realizability"
    1.64 +    (Scan.repeat1 Parse.string >> (Toplevel.theory o Extraction.add_realizes_eqns));
    1.65 +
    1.66 +val _ =
    1.67 +  Outer_Syntax.command @{command_spec "extract_type"}
    1.68 +    "add equations characterizing type of extracted program"
    1.69 +    (Scan.repeat1 Parse.string >> (Toplevel.theory o Extraction.add_typeof_eqns));
    1.70 +
    1.71 +val _ =
    1.72 +  Outer_Syntax.command @{command_spec "extract"} "extract terms from proofs"
    1.73 +    (Scan.repeat1 (Parse.xname -- parse_vars) >> (fn xs => Toplevel.theory (fn thy =>
    1.74 +      Extraction.extract (map (apfst (Global_Theory.get_thm thy)) xs) thy)));
    1.75 +
    1.76  
    1.77  
    1.78  (** end **)
     2.1 --- a/src/Pure/Isar/keyword.ML	Thu Aug 02 11:32:23 2012 +0200
     2.2 +++ b/src/Pure/Isar/keyword.ML	Thu Aug 02 12:36:54 2012 +0200
     2.3 @@ -43,7 +43,7 @@
     2.4    val tag_ml: T -> T
     2.5    type spec = string * string list
     2.6    val spec: spec -> T
     2.7 -  val command_spec: string * spec -> string * T
     2.8 +  val command_spec: (string * spec) * Position.T -> (string * T) * Position.T
     2.9    val get_lexicons: unit -> Scan.lexicon * Scan.lexicon
    2.10    val is_keyword: string -> bool
    2.11    val command_keyword: string -> T option
    2.12 @@ -135,7 +135,7 @@
    2.13      SOME k => k |> fold tag tags
    2.14    | NONE => error ("Unknown outer syntax keyword kind " ^ quote kind));
    2.15  
    2.16 -fun command_spec (name, s) = (name, spec s);
    2.17 +fun command_spec ((name, s), pos) = ((name, spec s), pos);
    2.18  
    2.19  
    2.20  
     3.1 --- a/src/Pure/Isar/outer_syntax.ML	Thu Aug 02 11:32:23 2012 +0200
     3.2 +++ b/src/Pure/Isar/outer_syntax.ML	Thu Aug 02 12:36:54 2012 +0200
     3.3 @@ -13,7 +13,7 @@
     3.4    val is_markup: outer_syntax -> Thy_Output.markup -> string -> bool
     3.5    val get_syntax: unit -> (Scan.lexicon * Scan.lexicon) * outer_syntax
     3.6    val check_syntax: unit -> unit
     3.7 -  type command_spec = string * Keyword.T
     3.8 +  type command_spec = (string * Keyword.T) * Position.T
     3.9    val command: command_spec -> string ->
    3.10      (Toplevel.transition -> Toplevel.transition) parser -> unit
    3.11    val markup_command: Thy_Output.markup -> command_spec -> string ->
    3.12 @@ -118,25 +118,26 @@
    3.13  
    3.14  (** global outer syntax **)
    3.15  
    3.16 -type command_spec = string * Keyword.T;
    3.17 +type command_spec = (string * Keyword.T) * Position.T;
    3.18  
    3.19  local
    3.20  
    3.21  (*synchronized wrt. Keywords*)
    3.22  val global_outer_syntax = Unsynchronized.ref empty_outer_syntax;
    3.23  
    3.24 -fun add_command (name, kind) cmd = CRITICAL (fn () =>
    3.25 +fun add_command ((name, kind), pos) cmd = CRITICAL (fn () =>
    3.26    let
    3.27      val thy = ML_Context.the_global_context ();
    3.28      val _ =
    3.29        (case try (Thy_Header.the_keyword thy) name of
    3.30          SOME spec =>
    3.31            if Option.map #1 spec = SOME (Keyword.kind_of kind) then ()
    3.32 -          else error ("Inconsistent outer syntax keyword declaration " ^ quote name)
    3.33 +          else error ("Inconsistent outer syntax keyword declaration " ^
    3.34 +            quote name ^ Position.str_of pos)
    3.35        | NONE =>
    3.36            if Context.theory_name thy = Context.PureN
    3.37            then Keyword.define (name, SOME kind)
    3.38 -          else error ("Undeclared outer syntax command " ^ quote name));
    3.39 +          else error ("Undeclared outer syntax command " ^ quote name ^ Position.str_of pos));
    3.40    in
    3.41      Unsynchronized.change global_outer_syntax (map_commands (fn commands =>
    3.42       (if not (Symtab.defined commands name) then ()
     4.1 --- a/src/Pure/ML/ml_antiquote.ML	Thu Aug 02 11:32:23 2012 +0200
     4.2 +++ b/src/Pure/ML/ml_antiquote.ML	Thu Aug 02 12:36:54 2012 +0200
     4.3 @@ -190,22 +190,26 @@
     4.4  
     4.5  fun with_keyword f =
     4.6    Args.theory -- Scan.lift (Parse.position Parse.string) >> (fn (thy, (name, pos)) =>
     4.7 -    (f (name, Thy_Header.the_keyword thy name)
     4.8 +    (f ((name, Thy_Header.the_keyword thy name), pos)
     4.9        handle ERROR msg => error (msg ^ Position.str_of pos)));
    4.10  
    4.11  val _ = Context.>> (Context.map_theory
    4.12   (value (Binding.name "keyword")
    4.13      (with_keyword
    4.14 -      (fn (name, NONE) => "Parse.$$$ " ^ ML_Syntax.print_string name
    4.15 -        | (name, SOME _) => error ("Expected minor keyword " ^ quote name))) #>
    4.16 +      (fn ((name, NONE), _) => "Parse.$$$ " ^ ML_Syntax.print_string name
    4.17 +        | ((name, SOME _), pos) =>
    4.18 +            error ("Expected minor keyword " ^ quote name ^ Position.str_of pos))) #>
    4.19    value (Binding.name "command_spec")
    4.20      (with_keyword
    4.21 -      (fn (name, SOME kind) =>
    4.22 +      (fn ((name, SOME kind), pos) =>
    4.23            "Keyword.command_spec " ^ ML_Syntax.atomic
    4.24 -            (ML_Syntax.print_pair ML_Syntax.print_string
    4.25 +            ((ML_Syntax.print_pair
    4.26                (ML_Syntax.print_pair ML_Syntax.print_string
    4.27 -                (ML_Syntax.print_list ML_Syntax.print_string)) (name, kind))
    4.28 -        | (name, NONE) => error ("Expected command keyword " ^ quote name)))));
    4.29 +                (ML_Syntax.print_pair ML_Syntax.print_string
    4.30 +                  (ML_Syntax.print_list ML_Syntax.print_string)))
    4.31 +              ML_Syntax.print_position) ((name, kind), pos))
    4.32 +        | ((name, NONE), pos) =>
    4.33 +            error ("Expected command keyword " ^ quote name ^ Position.str_of pos)))));
    4.34  
    4.35  end;
    4.36  
     5.1 --- a/src/Pure/Proof/extraction.ML	Thu Aug 02 11:32:23 2012 +0200
     5.2 +++ b/src/Pure/Proof/extraction.ML	Thu Aug 02 12:36:54 2012 +0200
     5.3 @@ -814,33 +814,6 @@
     5.4      |> Sign.restore_naming thy
     5.5    end;
     5.6  
     5.7 -
     5.8 -(**** interface ****)
     5.9 -
    5.10 -val parse_vars = Scan.optional (Parse.$$$ "(" |-- Parse.list1 Parse.name --| Parse.$$$ ")") [];
    5.11 -
    5.12 -val _ =
    5.13 -  Outer_Syntax.command ("realizers", Keyword.thy_decl)
    5.14 -    "specify realizers for primitive axioms / theorems, together with correctness proof"
    5.15 -    (Scan.repeat1 (Parse.xname -- parse_vars --| Parse.$$$ ":" -- Parse.string -- Parse.string) >>
    5.16 -     (fn xs => Toplevel.theory (fn thy => add_realizers
    5.17 -       (map (fn (((a, vs), s1), s2) => (Global_Theory.get_thm thy a, (vs, s1, s2))) xs) thy)));
    5.18 -
    5.19 -val _ =
    5.20 -  Outer_Syntax.command ("realizability", Keyword.thy_decl)
    5.21 -    "add equations characterizing realizability"
    5.22 -    (Scan.repeat1 Parse.string >> (Toplevel.theory o add_realizes_eqns));
    5.23 -
    5.24 -val _ =
    5.25 -  Outer_Syntax.command ("extract_type", Keyword.thy_decl)
    5.26 -    "add equations characterizing type of extracted program"
    5.27 -    (Scan.repeat1 Parse.string >> (Toplevel.theory o add_typeof_eqns));
    5.28 -
    5.29 -val _ =
    5.30 -  Outer_Syntax.command ("extract", Keyword.thy_decl) "extract terms from proofs"
    5.31 -    (Scan.repeat1 (Parse.xname -- parse_vars) >> (fn xs => Toplevel.theory (fn thy =>
    5.32 -      extract (map (apfst (Global_Theory.get_thm thy)) xs) thy)));
    5.33 -
    5.34  val etype_of = etype_of o add_syntax;
    5.35  
    5.36  end;
     6.1 --- a/src/Pure/ProofGeneral/proof_general_emacs.ML	Thu Aug 02 11:32:23 2012 +0200
     6.2 +++ b/src/Pure/ProofGeneral/proof_general_emacs.ML	Thu Aug 02 12:36:54 2012 +0200
     6.3 @@ -189,31 +189,37 @@
     6.4  (* additional outer syntax for Isar *)
     6.5  
     6.6  val _ =
     6.7 -  Outer_Syntax.improper_command ("ProofGeneral.pr", Keyword.diag) "print state (internal)"
     6.8 +  Outer_Syntax.improper_command
     6.9 +    (("ProofGeneral.pr", Keyword.diag), Position.none) "print state (internal)"
    6.10      (Scan.succeed (Toplevel.no_timing o Toplevel.keep (fn state =>
    6.11        if Toplevel.is_toplevel state orelse Toplevel.is_theory state then tell_clear_goals ()
    6.12        else (Toplevel.quiet := false; Toplevel.print_state true state))));
    6.13  
    6.14  val _ = (*undo without output -- historical*)
    6.15 -  Outer_Syntax.improper_command ("ProofGeneral.undo", Keyword.control) "(internal)"
    6.16 +  Outer_Syntax.improper_command
    6.17 +    (("ProofGeneral.undo", Keyword.control), Position.none) "(internal)"
    6.18      (Scan.succeed (Toplevel.no_timing o Toplevel.imperative (fn () => Isar.undo 1)));
    6.19  
    6.20  val _ =
    6.21 -  Outer_Syntax.improper_command ("ProofGeneral.restart", Keyword.control) "(internal)"
    6.22 +  Outer_Syntax.improper_command
    6.23 +    (("ProofGeneral.restart", Keyword.control), Position.none) "(internal)"
    6.24      (Parse.opt_unit >> (Toplevel.no_timing oo K (Toplevel.imperative restart)));
    6.25  
    6.26  val _ =
    6.27 -  Outer_Syntax.improper_command ("ProofGeneral.kill_proof", Keyword.control) "(internal)"
    6.28 +  Outer_Syntax.improper_command
    6.29 +    (("ProofGeneral.kill_proof", Keyword.control), Position.none) "(internal)"
    6.30      (Scan.succeed (Toplevel.no_timing o
    6.31        Toplevel.imperative (fn () => (Isar.kill_proof (); tell_clear_goals ()))));
    6.32  
    6.33  val _ =
    6.34 -  Outer_Syntax.improper_command ("ProofGeneral.inform_file_processed", Keyword.control) "(internal)"
    6.35 +  Outer_Syntax.improper_command
    6.36 +    (("ProofGeneral.inform_file_processed", Keyword.control), Position.none) "(internal)"
    6.37      (Parse.name >> (fn file =>
    6.38        Toplevel.no_timing o Toplevel.imperative (fn () => inform_file_processed file)));
    6.39  
    6.40  val _ =
    6.41 -  Outer_Syntax.improper_command ("ProofGeneral.inform_file_retracted", Keyword.control) "(internal)"
    6.42 +  Outer_Syntax.improper_command
    6.43 +    (("ProofGeneral.inform_file_retracted", Keyword.control), Position.none) "(internal)"
    6.44      (Parse.name >> (Toplevel.no_timing oo
    6.45        (fn file => Toplevel.imperative (fn () => inform_file_retracted file))));
    6.46  
     7.1 --- a/src/Pure/ProofGeneral/proof_general_pgip.ML	Thu Aug 02 11:32:23 2012 +0200
     7.2 +++ b/src/Pure/ProofGeneral/proof_general_pgip.ML	Thu Aug 02 12:36:54 2012 +0200
     7.3 @@ -1032,7 +1032,8 @@
     7.4  (* Extra command for embedding prover-control inside document (obscure/debug usage). *)
     7.5  
     7.6  val _ =
     7.7 -  Outer_Syntax.improper_command ("ProofGeneral.process_pgip", Keyword.control) "(internal)"
     7.8 +  Outer_Syntax.improper_command
     7.9 +    (("ProofGeneral.process_pgip", Keyword.control), Position.none) "(internal)"
    7.10      (Parse.text >> (Toplevel.no_timing oo
    7.11        (fn txt => Toplevel.imperative (fn () =>
    7.12          if print_mode_active proof_general_emacsN
     8.1 --- a/src/Pure/Pure.thy	Thu Aug 02 11:32:23 2012 +0200
     8.2 +++ b/src/Pure/Pure.thy	Thu Aug 02 12:36:54 2012 +0200
     8.3 @@ -80,8 +80,15 @@
     8.4    and "use_thy" "remove_thy" "kill_thy" :: control
     8.5    and "display_drafts" "print_drafts" "pr" :: diag
     8.6    and "disable_pr" "enable_pr" "commit" "quit" "exit" :: control
     8.7 +  and "welcome" :: diag
     8.8 +  and "init_toplevel" "linear_undo" "undo" "undos_proof" "cannot_undo" "kill" :: control
     8.9    and "end" :: thy_end % "theory"
    8.10 -  uses "Isar/isar_syn.ML"
    8.11 +  and "realizers" "realizability" "extract_type" "extract" :: thy_decl
    8.12 +  and "find_theorems" "find_consts" :: diag
    8.13 +  uses
    8.14 +    "Isar/isar_syn.ML"
    8.15 +    "Tools/find_theorems.ML"
    8.16 +    "Tools/find_consts.ML"
    8.17  begin
    8.18  
    8.19  section {* Further content for the Pure theory *}
     9.1 --- a/src/Pure/ROOT	Thu Aug 02 11:32:23 2012 +0200
     9.2 +++ b/src/Pure/ROOT	Thu Aug 02 12:36:54 2012 +0200
     9.3 @@ -196,8 +196,6 @@
     9.4      "Thy/thy_load.ML"
     9.5      "Thy/thy_output.ML"
     9.6      "Thy/thy_syntax.ML"
     9.7 -    "Tools/find_consts.ML"
     9.8 -    "Tools/find_theorems.ML"
     9.9      "Tools/named_thms.ML"
    9.10      "Tools/xml_syntax.ML"
    9.11      "assumption.ML"
    10.1 --- a/src/Pure/ROOT.ML	Thu Aug 02 11:32:23 2012 +0200
    10.2 +++ b/src/Pure/ROOT.ML	Thu Aug 02 12:36:54 2012 +0200
    10.3 @@ -282,9 +282,6 @@
    10.4  
    10.5  use "Tools/xml_syntax.ML";
    10.6  
    10.7 -use "Tools/find_theorems.ML";
    10.8 -use "Tools/find_consts.ML";
    10.9 -
   10.10  
   10.11  (* configuration for Proof General *)
   10.12  
    11.1 --- a/src/Pure/System/isar.ML	Thu Aug 02 11:32:23 2012 +0200
    11.2 +++ b/src/Pure/System/isar.ML	Thu Aug 02 12:36:54 2012 +0200
    11.3 @@ -151,51 +151,4 @@
    11.4    toplevel_loop TextIO.stdIn
    11.5      {init = true, welcome = true, sync = false, secure = Secure.is_secure ()};
    11.6  
    11.7 -
    11.8 -
    11.9 -(** command syntax **)
   11.10 -
   11.11 -local
   11.12 -
   11.13 -val op >> = Scan.>>;
   11.14 -
   11.15 -in
   11.16 -
   11.17 -(* global history *)
   11.18 -
   11.19 -val _ =
   11.20 -  Outer_Syntax.improper_command ("init_toplevel", Keyword.control) "init toplevel point-of-interest"
   11.21 -    (Scan.succeed (Toplevel.no_timing o Toplevel.imperative init));
   11.22 -
   11.23 -val _ =
   11.24 -  Outer_Syntax.improper_command ("linear_undo", Keyword.control) "undo commands"
   11.25 -    (Scan.optional Parse.nat 1 >>
   11.26 -      (fn n => Toplevel.no_timing o Toplevel.imperative (fn () => linear_undo n)));
   11.27 -
   11.28 -val _ =
   11.29 -  Outer_Syntax.improper_command ("undo", Keyword.control) "undo commands (skipping closed proofs)"
   11.30 -    (Scan.optional Parse.nat 1 >>
   11.31 -      (fn n => Toplevel.no_timing o Toplevel.imperative (fn () => undo n)));
   11.32 -
   11.33 -val _ =
   11.34 -  Outer_Syntax.improper_command ("undos_proof", Keyword.control)
   11.35 -    "undo commands (skipping closed proofs)"
   11.36 -    (Scan.optional Parse.nat 1 >> (fn n => Toplevel.no_timing o
   11.37 -      Toplevel.keep (fn state =>
   11.38 -        if Toplevel.is_proof state then (undo n; print ()) else raise Toplevel.UNDEF)));
   11.39 -
   11.40 -val _ =
   11.41 -  Outer_Syntax.improper_command ("cannot_undo", Keyword.control)
   11.42 -    "partial undo -- Proof General legacy"
   11.43 -    (Parse.name >>
   11.44 -      (fn "end" => Toplevel.no_timing o Toplevel.imperative (fn () => undo 1)
   11.45 -        | txt => Toplevel.imperative (fn () => error ("Cannot undo " ^ quote txt))));
   11.46 -
   11.47 -val _ =
   11.48 -  Outer_Syntax.improper_command ("kill", Keyword.control)
   11.49 -    "kill partial proof or theory development"
   11.50 -    (Scan.succeed (Toplevel.no_timing o Toplevel.imperative kill));
   11.51 -
   11.52  end;
   11.53 -
   11.54 -end;
    12.1 --- a/src/Pure/System/session.ML	Thu Aug 02 11:32:23 2012 +0200
    12.2 +++ b/src/Pure/System/session.ML	Thu Aug 02 12:36:54 2012 +0200
    12.3 @@ -47,10 +47,6 @@
    12.4      "Unofficial version of " ^ name () ^ " (" ^ Distribution.version ^ ")" ^
    12.5      (if Distribution.changelog <> "" then "\nSee also " ^ Distribution.changelog else "");
    12.6  
    12.7 -val _ =
    12.8 -  Outer_Syntax.improper_command ("welcome", Keyword.diag) "print welcome message"
    12.9 -    (Scan.succeed (Toplevel.no_timing o Toplevel.imperative (writeln o welcome)));
   12.10 -
   12.11  
   12.12  (* add_path *)
   12.13  
    13.1 --- a/src/Pure/Tools/find_consts.ML	Thu Aug 02 11:32:23 2012 +0200
    13.2 +++ b/src/Pure/Tools/find_consts.ML	Thu Aug 02 12:36:54 2012 +0200
    13.3 @@ -134,7 +134,7 @@
    13.4  in
    13.5  
    13.6  val _ =
    13.7 -  Outer_Syntax.improper_command ("find_consts", Keyword.diag) "search constants by type pattern"
    13.8 +  Outer_Syntax.improper_command @{command_spec "find_consts"} "search constants by type pattern"
    13.9      (Scan.repeat ((Scan.option Parse.minus >> is_none) -- criterion)
   13.10        >> (fn spec => Toplevel.no_timing o
   13.11          Toplevel.keep (fn state => find_consts (Toplevel.context_of state) spec)));
    14.1 --- a/src/Pure/Tools/find_theorems.ML	Thu Aug 02 11:32:23 2012 +0200
    14.2 +++ b/src/Pure/Tools/find_theorems.ML	Thu Aug 02 12:36:54 2012 +0200
    14.3 @@ -615,7 +615,7 @@
    14.4  val query_parser = Scan.repeat (((Scan.option Parse.minus >> is_none) -- criterion));
    14.5  
    14.6  val _ =
    14.7 -  Outer_Syntax.improper_command ("find_theorems", Keyword.diag)
    14.8 +  Outer_Syntax.improper_command @{command_spec "find_theorems"}
    14.9      "print theorems meeting specified criteria"
   14.10      (options -- query_parser
   14.11        >> (fn ((opt_lim, rem_dups), spec) =>
    15.1 --- a/src/Pure/pure_setup.ML	Thu Aug 02 11:32:23 2012 +0200
    15.2 +++ b/src/Pure/pure_setup.ML	Thu Aug 02 12:36:54 2012 +0200
    15.3 @@ -15,7 +15,8 @@
    15.4  (* the Pure theory *)
    15.5  
    15.6  val _ =
    15.7 -  Outer_Syntax.command ("theory", Keyword.tag_theory Keyword.thy_begin) "begin theory context"
    15.8 +  Outer_Syntax.command
    15.9 +    (("theory", Keyword.tag_theory Keyword.thy_begin), Position.none) "begin theory context"
   15.10      (Thy_Header.args >> (fn header =>
   15.11        Toplevel.print o
   15.12          Toplevel.init_theory