clarified bootstrap -- avoid 'ML_file' in Pure.thy for uniformity;
authorwenzelm
Mon Apr 04 17:25:53 2016 +0200 (2016-04-04)
changeset 62849caaa2fc4040d
parent 62848 e4140efe699e
child 62850 1f1a2c33ccf4
clarified bootstrap -- avoid 'ML_file' in Pure.thy for uniformity;
src/Pure/Isar/isar_syn.ML
src/Pure/Isar/outer_syntax.ML
src/Pure/ML/ml_file.ML
src/Pure/Pure.thy
src/Pure/ROOT
src/Pure/ROOT.ML
src/Pure/Thy/thy_header.ML
src/Pure/Thy/thy_header.scala
     1.1 --- a/src/Pure/Isar/isar_syn.ML	Mon Apr 04 17:02:34 2016 +0200
     1.2 +++ b/src/Pure/Isar/isar_syn.ML	Mon Apr 04 17:25:53 2016 +0200
     1.3 @@ -189,6 +189,23 @@
     1.4  
     1.5  (* use ML text *)
     1.6  
     1.7 +local
     1.8 +
     1.9 +fun ML_file_cmd debug files = Toplevel.generic_theory (fn gthy =>
    1.10 +  let
    1.11 +    val [{src_path, lines, digest, pos}: Token.file] = files (Context.theory_of gthy);
    1.12 +    val provide = Resources.provide (src_path, digest);
    1.13 +    val source = Input.source true (cat_lines lines) (pos, pos);
    1.14 +    val flags: ML_Compiler.flags =
    1.15 +      {SML = false, exchange = false, redirect = true, verbose = true,
    1.16 +        debug = debug, writeln = writeln, warning = warning};
    1.17 +  in
    1.18 +    gthy
    1.19 +    |> ML_Context.exec (fn () => ML_Context.eval_source flags source)
    1.20 +    |> Local_Theory.propagate_ml_env
    1.21 +    |> Context.mapping provide (Local_Theory.background_theory provide)
    1.22 +  end);
    1.23 +
    1.24  fun SML_file_cmd debug files = Toplevel.theory (fn thy =>
    1.25    let
    1.26      val ([{lines, pos, ...}: Token.file], thy') = files thy;
    1.27 @@ -201,6 +218,22 @@
    1.28        (ML_Context.exec (fn () => ML_Context.eval_source flags source))
    1.29    end);
    1.30  
    1.31 +in
    1.32 +
    1.33 +val _ =
    1.34 +  Outer_Syntax.command ("ML_file", @{here}) "read and evaluate Isabelle/ML file"
    1.35 +    (Resources.parse_files "ML_file" >> ML_file_cmd NONE);
    1.36 +
    1.37 +val _ =
    1.38 +  Outer_Syntax.command ("ML_file_debug", @{here})
    1.39 +    "read and evaluate Isabelle/ML file (with debugger information)"
    1.40 +    (Resources.parse_files "ML_file_debug" >> ML_file_cmd (SOME true));
    1.41 +
    1.42 +val _ =
    1.43 +  Outer_Syntax.command ("ML_file_no_debug", @{here})
    1.44 +    "read and evaluate Isabelle/ML file (no debugger information)"
    1.45 +    (Resources.parse_files "ML_file_no_debug" >> ML_file_cmd (SOME false));
    1.46 +
    1.47  val _ =
    1.48    Outer_Syntax.command @{command_keyword SML_file} "read and evaluate Standard ML file"
    1.49      (Resources.provide_parse_files "SML_file" >> SML_file_cmd NONE);
    1.50 @@ -215,6 +248,8 @@
    1.51      "read and evaluate Standard ML file (no debugger information)"
    1.52      (Resources.provide_parse_files "SML_file_no_debug" >> SML_file_cmd (SOME false));
    1.53  
    1.54 +end;
    1.55 +
    1.56  val _ =
    1.57    Outer_Syntax.command @{command_keyword SML_export} "evaluate SML within Isabelle/ML environment"
    1.58      (Parse.ML_source >> (fn source =>
    1.59 @@ -241,14 +276,6 @@
    1.60        end));
    1.61  
    1.62  val _ =
    1.63 -  Outer_Syntax.command @{command_keyword ML} "ML text within theory or local theory"
    1.64 -    (Parse.ML_source >> (fn source =>
    1.65 -      Toplevel.generic_theory
    1.66 -        (ML_Context.exec (fn () =>
    1.67 -            ML_Context.eval_source (ML_Compiler.verbose true ML_Compiler.flags) source) #>
    1.68 -          Local_Theory.propagate_ml_env)));
    1.69 -
    1.70 -val _ =
    1.71    Outer_Syntax.command @{command_keyword ML_prf} "ML text within proof"
    1.72      (Parse.ML_source >> (fn source =>
    1.73        Toplevel.proof (Proof.map_context (Context.proof_map
     2.1 --- a/src/Pure/Isar/outer_syntax.ML	Mon Apr 04 17:02:34 2016 +0200
     2.2 +++ b/src/Pure/Isar/outer_syntax.ML	Mon Apr 04 17:25:53 2016 +0200
     2.3 @@ -306,4 +306,15 @@
     2.4        in error ("Bad command " ^ quote name ^ Position.here pos ^ report) end
     2.5    end;
     2.6  
     2.7 +
     2.8 +(* 'ML' command -- required for bootstrapping Isar *)
     2.9 +
    2.10 +val _ =
    2.11 +  command ("ML", @{here}) "ML text within theory or local theory"
    2.12 +    (Parse.ML_source >> (fn source =>
    2.13 +      Toplevel.generic_theory
    2.14 +        (ML_Context.exec (fn () =>
    2.15 +            ML_Context.eval_source (ML_Compiler.verbose true ML_Compiler.flags) source) #>
    2.16 +          Local_Theory.propagate_ml_env)));
    2.17 +
    2.18  end;
     3.1 --- a/src/Pure/ML/ml_file.ML	Mon Apr 04 17:02:34 2016 +0200
     3.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     3.3 @@ -1,39 +0,0 @@
     3.4 -(*  Title:      Pure/ML/ml_file.ML
     3.5 -    Author:     Makarius
     3.6 -
     3.7 -The 'ML_file' command.
     3.8 -*)
     3.9 -
    3.10 -structure ML_File: sig end =
    3.11 -struct
    3.12 -
    3.13 -fun ML_file_cmd debug files = Toplevel.generic_theory (fn gthy =>
    3.14 -  let
    3.15 -    val [{src_path, lines, digest, pos}: Token.file] = files (Context.theory_of gthy);
    3.16 -    val provide = Resources.provide (src_path, digest);
    3.17 -    val source = Input.source true (cat_lines lines) (pos, pos);
    3.18 -    val flags: ML_Compiler.flags =
    3.19 -      {SML = false, exchange = false, redirect = true, verbose = true,
    3.20 -        debug = debug, writeln = writeln, warning = warning};
    3.21 -  in
    3.22 -    gthy
    3.23 -    |> ML_Context.exec (fn () => ML_Context.eval_source flags source)
    3.24 -    |> Local_Theory.propagate_ml_env
    3.25 -    |> Context.mapping provide (Local_Theory.background_theory provide)
    3.26 -  end);
    3.27 -
    3.28 -val _ =
    3.29 -  Outer_Syntax.command ("ML_file", @{here}) "read and evaluate Isabelle/ML file"
    3.30 -    (Resources.parse_files "ML_file" >> ML_file_cmd NONE);
    3.31 -
    3.32 -val _ =
    3.33 -  Outer_Syntax.command ("ML_file_debug", @{here})
    3.34 -    "read and evaluate Isabelle/ML file (with debugger information)"
    3.35 -    (Resources.parse_files "ML_file_debug" >> ML_file_cmd (SOME true));
    3.36 -
    3.37 -val _ =
    3.38 -  Outer_Syntax.command ("ML_file_no_debug", @{here})
    3.39 -    "read and evaluate Isabelle/ML file (no debugger information)"
    3.40 -    (Resources.parse_files "ML_file_no_debug" >> ML_file_cmd (SOME false));
    3.41 -
    3.42 -end;
     4.1 --- a/src/Pure/Pure.thy	Mon Apr 04 17:02:34 2016 +0200
     4.2 +++ b/src/Pure/Pure.thy	Mon Apr 04 17:25:53 2016 +0200
     4.3 @@ -21,9 +21,9 @@
     4.4      "definition" "abbreviation" "type_notation" "no_type_notation" "notation"
     4.5      "no_notation" "axiomatization" "lemmas" "declare"
     4.6      "hide_class" "hide_type" "hide_const" "hide_fact" :: thy_decl
     4.7 +  and "ML_file" "ML_file_debug" "ML_file_no_debug" :: thy_load % "ML"
     4.8    and "SML_file" "SML_file_debug" "SML_file_no_debug" :: thy_load % "ML"
     4.9    and "SML_import" "SML_export" :: thy_decl % "ML"
    4.10 -  and "ML" :: thy_decl % "ML"
    4.11    and "ML_prf" :: prf_decl % "proof"  (* FIXME % "ML" ?? *)
    4.12    and "ML_val" "ML_command" :: diag % "ML"
    4.13    and "simproc_setup" :: thy_decl % "ML" == ""
    4.14 @@ -93,7 +93,1130 @@
    4.15    and "named_theorems" :: thy_decl
    4.16  begin
    4.17  
    4.18 -ML_file "Isar/isar_syn.ML"
    4.19 +section \<open>Isar commands\<close>
    4.20 +
    4.21 +ML \<open>
    4.22 +local
    4.23 +
    4.24 +(** theory commands **)
    4.25 +
    4.26 +(* sorts *)
    4.27 +
    4.28 +val _ =
    4.29 +  Outer_Syntax.local_theory @{command_keyword default_sort}
    4.30 +    "declare default sort for explicit type variables"
    4.31 +    (Parse.sort >> (fn s => fn lthy => Local_Theory.set_defsort (Syntax.read_sort lthy s) lthy));
    4.32 +
    4.33 +
    4.34 +(* types *)
    4.35 +
    4.36 +val _ =
    4.37 +  Outer_Syntax.local_theory @{command_keyword typedecl} "type declaration"
    4.38 +    (Parse.type_args -- Parse.binding -- Parse.opt_mixfix
    4.39 +      >> (fn ((args, a), mx) =>
    4.40 +          Typedecl.typedecl {final = true} (a, map (rpair dummyS) args, mx) #> snd));
    4.41 +
    4.42 +val _ =
    4.43 +  Outer_Syntax.local_theory @{command_keyword type_synonym} "declare type abbreviation"
    4.44 +    (Parse.type_args -- Parse.binding --
    4.45 +      (@{keyword "="} |-- Parse.!!! (Parse.typ -- Parse.opt_mixfix'))
    4.46 +      >> (fn ((args, a), (rhs, mx)) => snd o Typedecl.abbrev_cmd (a, args, mx) rhs));
    4.47 +
    4.48 +val _ =
    4.49 +  Outer_Syntax.command @{command_keyword nonterminal}
    4.50 +    "declare syntactic type constructors (grammar nonterminal symbols)"
    4.51 +    (Parse.and_list1 Parse.binding >> (Toplevel.theory o Sign.add_nonterminals_global));
    4.52 +
    4.53 +
    4.54 +(* consts and syntax *)
    4.55 +
    4.56 +val _ =
    4.57 +  Outer_Syntax.command @{command_keyword judgment} "declare object-logic judgment"
    4.58 +    (Parse.const_binding >> (Toplevel.theory o Object_Logic.add_judgment_cmd));
    4.59 +
    4.60 +val _ =
    4.61 +  Outer_Syntax.command @{command_keyword consts} "declare constants"
    4.62 +    (Scan.repeat1 Parse.const_binding >> (Toplevel.theory o Sign.add_consts_cmd));
    4.63 +
    4.64 +val mode_spec =
    4.65 +  (@{keyword "output"} >> K ("", false)) ||
    4.66 +    Parse.name -- Scan.optional (@{keyword "output"} >> K false) true;
    4.67 +
    4.68 +val opt_mode =
    4.69 +  Scan.optional (@{keyword "("} |-- Parse.!!! (mode_spec --| @{keyword ")"})) Syntax.mode_default;
    4.70 +
    4.71 +val _ =
    4.72 +  Outer_Syntax.command @{command_keyword syntax} "add raw syntax clauses"
    4.73 +    (opt_mode -- Scan.repeat1 Parse.const_decl
    4.74 +      >> (Toplevel.theory o uncurry Sign.add_syntax_cmd));
    4.75 +
    4.76 +val _ =
    4.77 +  Outer_Syntax.command @{command_keyword no_syntax} "delete raw syntax clauses"
    4.78 +    (opt_mode -- Scan.repeat1 Parse.const_decl
    4.79 +      >> (Toplevel.theory o uncurry Sign.del_syntax_cmd));
    4.80 +
    4.81 +
    4.82 +(* translations *)
    4.83 +
    4.84 +val trans_pat =
    4.85 +  Scan.optional
    4.86 +    (@{keyword "("} |-- Parse.!!! (Parse.inner_syntax Parse.xname --| @{keyword ")"})) "logic"
    4.87 +    -- Parse.inner_syntax Parse.string;
    4.88 +
    4.89 +fun trans_arrow toks =
    4.90 +  ((@{keyword "\<rightharpoonup>"} || @{keyword "=>"}) >> K Syntax.Parse_Rule ||
    4.91 +    (@{keyword "\<leftharpoondown>"} || @{keyword "<="}) >> K Syntax.Print_Rule ||
    4.92 +    (@{keyword "\<rightleftharpoons>"} || @{keyword "=="}) >> K Syntax.Parse_Print_Rule) toks;
    4.93 +
    4.94 +val trans_line =
    4.95 +  trans_pat -- Parse.!!! (trans_arrow -- trans_pat)
    4.96 +    >> (fn (left, (arr, right)) => arr (left, right));
    4.97 +
    4.98 +val _ =
    4.99 +  Outer_Syntax.command @{command_keyword translations} "add syntax translation rules"
   4.100 +    (Scan.repeat1 trans_line >> (Toplevel.theory o Isar_Cmd.translations));
   4.101 +
   4.102 +val _ =
   4.103 +  Outer_Syntax.command @{command_keyword no_translations} "delete syntax translation rules"
   4.104 +    (Scan.repeat1 trans_line >> (Toplevel.theory o Isar_Cmd.no_translations));
   4.105 +
   4.106 +
   4.107 +(* constant definitions and abbreviations *)
   4.108 +
   4.109 +val _ =
   4.110 +  Outer_Syntax.local_theory' @{command_keyword definition} "constant definition"
   4.111 +    (Parse_Spec.constdef >> (fn args => #2 oo Specification.definition_cmd args));
   4.112 +
   4.113 +val _ =
   4.114 +  Outer_Syntax.local_theory' @{command_keyword abbreviation} "constant abbreviation"
   4.115 +    (opt_mode -- (Scan.option Parse_Spec.constdecl -- Parse.prop)
   4.116 +      >> (fn (mode, args) => Specification.abbreviation_cmd mode args));
   4.117 +
   4.118 +val _ =
   4.119 +  Outer_Syntax.local_theory @{command_keyword type_notation}
   4.120 +    "add concrete syntax for type constructors"
   4.121 +    (opt_mode -- Parse.and_list1 (Parse.type_const -- Parse.mixfix)
   4.122 +      >> (fn (mode, args) => Specification.type_notation_cmd true mode args));
   4.123 +
   4.124 +val _ =
   4.125 +  Outer_Syntax.local_theory @{command_keyword no_type_notation}
   4.126 +    "delete concrete syntax for type constructors"
   4.127 +    (opt_mode -- Parse.and_list1 (Parse.type_const -- Parse.mixfix)
   4.128 +      >> (fn (mode, args) => Specification.type_notation_cmd false mode args));
   4.129 +
   4.130 +val _ =
   4.131 +  Outer_Syntax.local_theory @{command_keyword notation}
   4.132 +    "add concrete syntax for constants / fixed variables"
   4.133 +    (opt_mode -- Parse.and_list1 (Parse.const -- Parse.mixfix)
   4.134 +      >> (fn (mode, args) => Specification.notation_cmd true mode args));
   4.135 +
   4.136 +val _ =
   4.137 +  Outer_Syntax.local_theory @{command_keyword no_notation}
   4.138 +    "delete concrete syntax for constants / fixed variables"
   4.139 +    (opt_mode -- Parse.and_list1 (Parse.const -- Parse.mixfix)
   4.140 +      >> (fn (mode, args) => Specification.notation_cmd false mode args));
   4.141 +
   4.142 +
   4.143 +(* constant specifications *)
   4.144 +
   4.145 +val _ =
   4.146 +  Outer_Syntax.command @{command_keyword axiomatization} "axiomatic constant specification"
   4.147 +    (Scan.optional Parse.fixes [] --
   4.148 +      Scan.optional (Parse.where_ |-- Parse.!!! (Parse.and_list1 Parse_Spec.specs)) []
   4.149 +      >> (fn (x, y) => Toplevel.theory (#2 o Specification.axiomatization_cmd x y)));
   4.150 +
   4.151 +
   4.152 +(* theorems *)
   4.153 +
   4.154 +val _ =
   4.155 +  Outer_Syntax.local_theory' @{command_keyword lemmas} "define theorems"
   4.156 +    (Parse_Spec.name_facts -- Parse.for_fixes >>
   4.157 +      (fn (facts, fixes) => #2 oo Specification.theorems_cmd Thm.theoremK facts fixes));
   4.158 +
   4.159 +val _ =
   4.160 +  Outer_Syntax.local_theory' @{command_keyword declare} "declare theorems"
   4.161 +    (Parse.and_list1 Parse.xthms1 -- Parse.for_fixes
   4.162 +      >> (fn (facts, fixes) =>
   4.163 +          #2 oo Specification.theorems_cmd "" [(Attrib.empty_binding, flat facts)] fixes));
   4.164 +
   4.165 +val _ =
   4.166 +  Outer_Syntax.local_theory @{command_keyword named_theorems}
   4.167 +    "declare named collection of theorems"
   4.168 +    (Parse.and_list1 (Parse.binding -- Scan.optional Parse.text "") >>
   4.169 +      fold (fn (b, descr) => snd o Named_Theorems.declare b descr));
   4.170 +
   4.171 +
   4.172 +(* hide names *)
   4.173 +
   4.174 +local
   4.175 +
   4.176 +fun hide_names command_keyword what hide parse prep =
   4.177 +  Outer_Syntax.command command_keyword ("hide " ^ what ^ " from name space")
   4.178 +    ((Parse.opt_keyword "open" >> not) -- Scan.repeat1 parse >> (fn (fully, args) =>
   4.179 +      (Toplevel.theory (fn thy =>
   4.180 +        let val ctxt = Proof_Context.init_global thy
   4.181 +        in fold (hide fully o prep ctxt) args thy end))));
   4.182 +
   4.183 +in
   4.184 +
   4.185 +val _ =
   4.186 +  hide_names @{command_keyword hide_class} "classes" Sign.hide_class Parse.class
   4.187 +    Proof_Context.read_class;
   4.188 +
   4.189 +val _ =
   4.190 +  hide_names @{command_keyword hide_type} "types" Sign.hide_type Parse.type_const
   4.191 +    ((#1 o dest_Type) oo Proof_Context.read_type_name {proper = true, strict = false});
   4.192 +
   4.193 +val _ =
   4.194 +  hide_names @{command_keyword hide_const} "consts" Sign.hide_const Parse.const
   4.195 +    ((#1 o dest_Const) oo Proof_Context.read_const {proper = true, strict = false});
   4.196 +
   4.197 +val _ =
   4.198 +  hide_names @{command_keyword hide_fact} "facts" Global_Theory.hide_fact
   4.199 +    (Parse.position Parse.xname) (Global_Theory.check_fact o Proof_Context.theory_of);
   4.200 +
   4.201 +end;
   4.202 +
   4.203 +
   4.204 +(* use ML text *)
   4.205 +
   4.206 +local
   4.207 +
   4.208 +fun ML_file_cmd debug files = Toplevel.generic_theory (fn gthy =>
   4.209 +  let
   4.210 +    val [{src_path, lines, digest, pos}: Token.file] = files (Context.theory_of gthy);
   4.211 +    val provide = Resources.provide (src_path, digest);
   4.212 +    val source = Input.source true (cat_lines lines) (pos, pos);
   4.213 +    val flags: ML_Compiler.flags =
   4.214 +      {SML = false, exchange = false, redirect = true, verbose = true,
   4.215 +        debug = debug, writeln = writeln, warning = warning};
   4.216 +  in
   4.217 +    gthy
   4.218 +    |> ML_Context.exec (fn () => ML_Context.eval_source flags source)
   4.219 +    |> Local_Theory.propagate_ml_env
   4.220 +    |> Context.mapping provide (Local_Theory.background_theory provide)
   4.221 +  end);
   4.222 +
   4.223 +fun SML_file_cmd debug files = Toplevel.theory (fn thy =>
   4.224 +  let
   4.225 +    val ([{lines, pos, ...}: Token.file], thy') = files thy;
   4.226 +    val source = Input.source true (cat_lines lines) (pos, pos);
   4.227 +    val flags: ML_Compiler.flags =
   4.228 +      {SML = true, exchange = false, redirect = true, verbose = true,
   4.229 +        debug = debug, writeln = writeln, warning = warning};
   4.230 +  in
   4.231 +    thy' |> Context.theory_map
   4.232 +      (ML_Context.exec (fn () => ML_Context.eval_source flags source))
   4.233 +  end);
   4.234 +
   4.235 +in
   4.236 +
   4.237 +val _ =
   4.238 +  Outer_Syntax.command ("ML_file", @{here}) "read and evaluate Isabelle/ML file"
   4.239 +    (Resources.parse_files "ML_file" >> ML_file_cmd NONE);
   4.240 +
   4.241 +val _ =
   4.242 +  Outer_Syntax.command ("ML_file_debug", @{here})
   4.243 +    "read and evaluate Isabelle/ML file (with debugger information)"
   4.244 +    (Resources.parse_files "ML_file_debug" >> ML_file_cmd (SOME true));
   4.245 +
   4.246 +val _ =
   4.247 +  Outer_Syntax.command ("ML_file_no_debug", @{here})
   4.248 +    "read and evaluate Isabelle/ML file (no debugger information)"
   4.249 +    (Resources.parse_files "ML_file_no_debug" >> ML_file_cmd (SOME false));
   4.250 +
   4.251 +val _ =
   4.252 +  Outer_Syntax.command @{command_keyword SML_file} "read and evaluate Standard ML file"
   4.253 +    (Resources.provide_parse_files "SML_file" >> SML_file_cmd NONE);
   4.254 +
   4.255 +val _ =
   4.256 +  Outer_Syntax.command @{command_keyword SML_file_debug}
   4.257 +    "read and evaluate Standard ML file (with debugger information)"
   4.258 +    (Resources.provide_parse_files "SML_file_debug" >> SML_file_cmd (SOME true));
   4.259 +
   4.260 +val _ =
   4.261 +  Outer_Syntax.command @{command_keyword SML_file_no_debug}
   4.262 +    "read and evaluate Standard ML file (no debugger information)"
   4.263 +    (Resources.provide_parse_files "SML_file_no_debug" >> SML_file_cmd (SOME false));
   4.264 +
   4.265 +end;
   4.266 +
   4.267 +val _ =
   4.268 +  Outer_Syntax.command @{command_keyword SML_export} "evaluate SML within Isabelle/ML environment"
   4.269 +    (Parse.ML_source >> (fn source =>
   4.270 +      let
   4.271 +        val flags: ML_Compiler.flags =
   4.272 +          {SML = true, exchange = true, redirect = false, verbose = true,
   4.273 +            debug = NONE, writeln = writeln, warning = warning};
   4.274 +      in
   4.275 +        Toplevel.theory
   4.276 +          (Context.theory_map (ML_Context.exec (fn () => ML_Context.eval_source flags source)))
   4.277 +      end));
   4.278 +
   4.279 +val _ =
   4.280 +  Outer_Syntax.command @{command_keyword SML_import} "evaluate Isabelle/ML within SML environment"
   4.281 +    (Parse.ML_source >> (fn source =>
   4.282 +      let
   4.283 +        val flags: ML_Compiler.flags =
   4.284 +          {SML = false, exchange = true, redirect = false, verbose = true,
   4.285 +            debug = NONE, writeln = writeln, warning = warning};
   4.286 +      in
   4.287 +        Toplevel.generic_theory
   4.288 +          (ML_Context.exec (fn () => ML_Context.eval_source flags source) #>
   4.289 +            Local_Theory.propagate_ml_env)
   4.290 +      end));
   4.291 +
   4.292 +val _ =
   4.293 +  Outer_Syntax.command @{command_keyword ML_prf} "ML text within proof"
   4.294 +    (Parse.ML_source >> (fn source =>
   4.295 +      Toplevel.proof (Proof.map_context (Context.proof_map
   4.296 +        (ML_Context.exec (fn () =>
   4.297 +            ML_Context.eval_source (ML_Compiler.verbose true ML_Compiler.flags) source))) #>
   4.298 +          Proof.propagate_ml_env)));
   4.299 +
   4.300 +val _ =
   4.301 +  Outer_Syntax.command @{command_keyword ML_val} "diagnostic ML text"
   4.302 +    (Parse.ML_source >> Isar_Cmd.ml_diag true);
   4.303 +
   4.304 +val _ =
   4.305 +  Outer_Syntax.command @{command_keyword ML_command} "diagnostic ML text (silent)"
   4.306 +    (Parse.ML_source >> Isar_Cmd.ml_diag false);
   4.307 +
   4.308 +val _ =
   4.309 +  Outer_Syntax.command @{command_keyword setup} "ML setup for global theory"
   4.310 +    (Parse.ML_source >> (Toplevel.theory o Isar_Cmd.setup));
   4.311 +
   4.312 +val _ =
   4.313 +  Outer_Syntax.local_theory @{command_keyword local_setup} "ML setup for local theory"
   4.314 +    (Parse.ML_source >> Isar_Cmd.local_setup);
   4.315 +
   4.316 +val _ =
   4.317 +  Outer_Syntax.local_theory @{command_keyword attribute_setup} "define attribute in ML"
   4.318 +    (Parse.position Parse.name --
   4.319 +        Parse.!!! (@{keyword "="} |-- Parse.ML_source -- Scan.optional Parse.text "")
   4.320 +      >> (fn (name, (txt, cmt)) => Attrib.attribute_setup name txt cmt));
   4.321 +
   4.322 +val _ =
   4.323 +  Outer_Syntax.local_theory @{command_keyword method_setup} "define proof method in ML"
   4.324 +    (Parse.position Parse.name --
   4.325 +        Parse.!!! (@{keyword "="} |-- Parse.ML_source -- Scan.optional Parse.text "")
   4.326 +      >> (fn (name, (txt, cmt)) => Method.method_setup name txt cmt));
   4.327 +
   4.328 +val _ =
   4.329 +  Outer_Syntax.local_theory @{command_keyword declaration} "generic ML declaration"
   4.330 +    (Parse.opt_keyword "pervasive" -- Parse.ML_source
   4.331 +      >> (fn (pervasive, txt) => Isar_Cmd.declaration {syntax = false, pervasive = pervasive} txt));
   4.332 +
   4.333 +val _ =
   4.334 +  Outer_Syntax.local_theory @{command_keyword syntax_declaration} "generic ML syntax declaration"
   4.335 +    (Parse.opt_keyword "pervasive" -- Parse.ML_source
   4.336 +      >> (fn (pervasive, txt) => Isar_Cmd.declaration {syntax = true, pervasive = pervasive} txt));
   4.337 +
   4.338 +val _ =
   4.339 +  Outer_Syntax.local_theory @{command_keyword simproc_setup} "define simproc in ML"
   4.340 +    (Parse.position Parse.name --
   4.341 +      (@{keyword "("} |-- Parse.enum1 "|" Parse.term --| @{keyword ")"} --| @{keyword "="}) --
   4.342 +      Parse.ML_source -- Scan.optional (@{keyword "identifier"} |-- Scan.repeat1 Parse.xname) []
   4.343 +    >> (fn (((a, b), c), d) => Isar_Cmd.simproc_setup a b c d));
   4.344 +
   4.345 +
   4.346 +(* translation functions *)
   4.347 +
   4.348 +val _ =
   4.349 +  Outer_Syntax.command @{command_keyword parse_ast_translation}
   4.350 +    "install parse ast translation functions"
   4.351 +    (Parse.ML_source >> (Toplevel.theory o Isar_Cmd.parse_ast_translation));
   4.352 +
   4.353 +val _ =
   4.354 +  Outer_Syntax.command @{command_keyword parse_translation}
   4.355 +    "install parse translation functions"
   4.356 +    (Parse.ML_source >> (Toplevel.theory o Isar_Cmd.parse_translation));
   4.357 +
   4.358 +val _ =
   4.359 +  Outer_Syntax.command @{command_keyword print_translation}
   4.360 +    "install print translation functions"
   4.361 +    (Parse.ML_source >> (Toplevel.theory o Isar_Cmd.print_translation));
   4.362 +
   4.363 +val _ =
   4.364 +  Outer_Syntax.command @{command_keyword typed_print_translation}
   4.365 +    "install typed print translation functions"
   4.366 +    (Parse.ML_source >> (Toplevel.theory o Isar_Cmd.typed_print_translation));
   4.367 +
   4.368 +val _ =
   4.369 +  Outer_Syntax.command @{command_keyword print_ast_translation}
   4.370 +    "install print ast translation functions"
   4.371 +    (Parse.ML_source >> (Toplevel.theory o Isar_Cmd.print_ast_translation));
   4.372 +
   4.373 +
   4.374 +(* oracles *)
   4.375 +
   4.376 +val _ =
   4.377 +  Outer_Syntax.command @{command_keyword oracle} "declare oracle"
   4.378 +    (Parse.range Parse.name -- (@{keyword "="} |-- Parse.ML_source) >>
   4.379 +      (fn (x, y) => Toplevel.theory (Isar_Cmd.oracle x y)));
   4.380 +
   4.381 +
   4.382 +(* bundled declarations *)
   4.383 +
   4.384 +val _ =
   4.385 +  Outer_Syntax.local_theory @{command_keyword bundle} "define bundle of declarations"
   4.386 +    ((Parse.binding --| @{keyword "="}) -- Parse.xthms1 -- Parse.for_fixes
   4.387 +      >> (uncurry Bundle.bundle_cmd));
   4.388 +
   4.389 +val _ =
   4.390 +  Outer_Syntax.command @{command_keyword include}
   4.391 +    "include declarations from bundle in proof body"
   4.392 +    (Scan.repeat1 (Parse.position Parse.xname) >> (Toplevel.proof o Bundle.include_cmd));
   4.393 +
   4.394 +val _ =
   4.395 +  Outer_Syntax.command @{command_keyword including}
   4.396 +    "include declarations from bundle in goal refinement"
   4.397 +    (Scan.repeat1 (Parse.position Parse.xname) >> (Toplevel.proof o Bundle.including_cmd));
   4.398 +
   4.399 +val _ =
   4.400 +  Outer_Syntax.command @{command_keyword print_bundles}
   4.401 +    "print bundles of declarations"
   4.402 +    (Parse.opt_bang >> (fn b => Toplevel.keep (Bundle.print_bundles b o Toplevel.context_of)));
   4.403 +
   4.404 +
   4.405 +(* local theories *)
   4.406 +
   4.407 +val _ =
   4.408 +  Outer_Syntax.command @{command_keyword context} "begin local theory context"
   4.409 +    ((Parse.position Parse.xname >> (fn name =>
   4.410 +        Toplevel.begin_local_theory true (Named_Target.begin name)) ||
   4.411 +      Scan.optional Parse_Spec.includes [] -- Scan.repeat Parse_Spec.context_element
   4.412 +        >> (fn (incls, elems) => Toplevel.open_target (#2 o Bundle.context_cmd incls elems)))
   4.413 +      --| Parse.begin);
   4.414 +
   4.415 +
   4.416 +(* locales *)
   4.417 +
   4.418 +val locale_val =
   4.419 +  Parse_Spec.locale_expression --
   4.420 +    Scan.optional (@{keyword "+"} |-- Parse.!!! (Scan.repeat1 Parse_Spec.context_element)) [] ||
   4.421 +  Scan.repeat1 Parse_Spec.context_element >> pair ([], []);
   4.422 +
   4.423 +val _ =
   4.424 +  Outer_Syntax.command @{command_keyword locale} "define named specification context"
   4.425 +    (Parse.binding --
   4.426 +      Scan.optional (@{keyword "="} |-- Parse.!!! locale_val) (([], []), []) -- Parse.opt_begin
   4.427 +      >> (fn ((name, (expr, elems)), begin) =>
   4.428 +          Toplevel.begin_local_theory begin
   4.429 +            (Expression.add_locale_cmd name Binding.empty expr elems #> snd)));
   4.430 +
   4.431 +val _ =
   4.432 +  Outer_Syntax.command @{command_keyword experiment} "open private specification context"
   4.433 +    (Scan.repeat Parse_Spec.context_element --| Parse.begin
   4.434 +      >> (fn elems =>
   4.435 +          Toplevel.begin_local_theory true (Experiment.experiment_cmd elems #> snd)));
   4.436 +
   4.437 +val interpretation_args =
   4.438 +  Parse.!!! Parse_Spec.locale_expression --
   4.439 +    Scan.optional
   4.440 +      (@{keyword "rewrites"} |-- Parse.and_list1 (Parse_Spec.opt_thm_name ":" -- Parse.prop)) [];
   4.441 +
   4.442 +val _ =
   4.443 +  Outer_Syntax.command @{command_keyword interpret}
   4.444 +    "prove interpretation of locale expression in proof context"
   4.445 +    (interpretation_args >> (fn (expr, equations) =>
   4.446 +      Toplevel.proof (Interpretation.interpret_cmd expr equations)));
   4.447 +
   4.448 +val interpretation_args_with_defs =
   4.449 +  Parse.!!! Parse_Spec.locale_expression --
   4.450 +    (Scan.optional (@{keyword "defines"} |-- Parse.and_list1 (Parse_Spec.opt_thm_name ":"
   4.451 +      -- ((Parse.binding -- Parse.opt_mixfix') --| @{keyword "="} -- Parse.term))) [] --
   4.452 +    Scan.optional
   4.453 +      (@{keyword "rewrites"} |-- Parse.and_list1 (Parse_Spec.opt_thm_name ":" -- Parse.prop)) []);
   4.454 +
   4.455 +val _ =
   4.456 +  Outer_Syntax.local_theory_to_proof @{command_keyword global_interpretation}
   4.457 +    "prove interpretation of locale expression into global theory"
   4.458 +    (interpretation_args_with_defs
   4.459 +      >> (fn (expr, (defs, equations)) => Interpretation.global_interpretation_cmd expr defs equations));
   4.460 +
   4.461 +val _ =
   4.462 +  Outer_Syntax.command @{command_keyword sublocale}
   4.463 +    "prove sublocale relation between a locale and a locale expression"
   4.464 +    ((Parse.position Parse.xname --| (@{keyword "\<subseteq>"} || @{keyword "<"}) --
   4.465 +      interpretation_args_with_defs >> (fn (loc, (expr, (defs, equations))) =>
   4.466 +        Toplevel.theory_to_proof (Interpretation.global_sublocale_cmd loc expr defs equations)))
   4.467 +    || interpretation_args_with_defs >> (fn (expr, (defs, equations)) =>
   4.468 +        Toplevel.local_theory_to_proof NONE NONE (Interpretation.sublocale_cmd expr defs equations)));
   4.469 +
   4.470 +val _ =
   4.471 +  Outer_Syntax.command @{command_keyword interpretation}
   4.472 +    "prove interpretation of locale expression in local theory or into global theory"
   4.473 +    (interpretation_args >> (fn (expr, equations) =>
   4.474 +      Toplevel.local_theory_to_proof NONE NONE (Interpretation.isar_interpretation_cmd expr equations)));
   4.475 +
   4.476 +
   4.477 +
   4.478 +(* classes *)
   4.479 +
   4.480 +val class_val =
   4.481 +  Parse_Spec.class_expression --
   4.482 +    Scan.optional (@{keyword "+"} |-- Parse.!!! (Scan.repeat1 Parse_Spec.context_element)) [] ||
   4.483 +  Scan.repeat1 Parse_Spec.context_element >> pair [];
   4.484 +
   4.485 +val _ =
   4.486 +  Outer_Syntax.command @{command_keyword class} "define type class"
   4.487 +   (Parse.binding -- Scan.optional (@{keyword "="} |-- class_val) ([], []) -- Parse.opt_begin
   4.488 +    >> (fn ((name, (supclasses, elems)), begin) =>
   4.489 +        Toplevel.begin_local_theory begin
   4.490 +          (Class_Declaration.class_cmd name supclasses elems #> snd)));
   4.491 +
   4.492 +val _ =
   4.493 +  Outer_Syntax.local_theory_to_proof @{command_keyword subclass} "prove a subclass relation"
   4.494 +    (Parse.class >> Class_Declaration.subclass_cmd);
   4.495 +
   4.496 +val _ =
   4.497 +  Outer_Syntax.command @{command_keyword instantiation} "instantiate and prove type arity"
   4.498 +   (Parse.multi_arity --| Parse.begin
   4.499 +     >> (fn arities => Toplevel.begin_local_theory true (Class.instantiation_cmd arities)));
   4.500 +
   4.501 +val _ =
   4.502 +  Outer_Syntax.command @{command_keyword instance} "prove type arity or subclass relation"
   4.503 +  ((Parse.class --
   4.504 +    ((@{keyword "\<subseteq>"} || @{keyword "<"}) |-- Parse.!!! Parse.class) >> Class.classrel_cmd ||
   4.505 +    Parse.multi_arity >> Class.instance_arity_cmd) >> Toplevel.theory_to_proof ||
   4.506 +    Scan.succeed (Toplevel.local_theory_to_proof NONE NONE (Class.instantiation_instance I)));
   4.507 +
   4.508 +
   4.509 +(* arbitrary overloading *)
   4.510 +
   4.511 +val _ =
   4.512 +  Outer_Syntax.command @{command_keyword overloading} "overloaded definitions"
   4.513 +   (Scan.repeat1 (Parse.name --| (@{keyword "=="} || @{keyword "\<equiv>"}) -- Parse.term --
   4.514 +      Scan.optional (@{keyword "("} |-- (@{keyword "unchecked"} >> K false) --| @{keyword ")"}) true
   4.515 +      >> Scan.triple1) --| Parse.begin
   4.516 +   >> (fn operations => Toplevel.begin_local_theory true (Overloading.overloading_cmd operations)));
   4.517 +
   4.518 +
   4.519 +(* code generation *)
   4.520 +
   4.521 +val _ =
   4.522 +  Outer_Syntax.command @{command_keyword code_datatype}
   4.523 +    "define set of code datatype constructors"
   4.524 +    (Scan.repeat1 Parse.term >> (Toplevel.theory o Code.add_datatype_cmd));
   4.525 +
   4.526 +
   4.527 +
   4.528 +(** proof commands **)
   4.529 +
   4.530 +val _ =
   4.531 +  Outer_Syntax.local_theory_to_proof @{command_keyword notepad} "begin proof context"
   4.532 +    (Parse.begin >> K Proof.begin_notepad);
   4.533 +
   4.534 +
   4.535 +(* statements *)
   4.536 +
   4.537 +val structured_statement =
   4.538 +  Parse_Spec.statement -- Parse_Spec.cond_statement -- Parse.for_fixes
   4.539 +    >> (fn ((shows, (strict, assumes)), fixes) => (strict, fixes, assumes, shows));
   4.540 +
   4.541 +val structured_statement' =
   4.542 +  Parse_Spec.statement -- Parse_Spec.if_statement' -- Parse.for_fixes
   4.543 +    >> (fn ((shows, assumes), fixes) => (fixes, assumes, shows));
   4.544 +
   4.545 +
   4.546 +fun theorem spec schematic descr =
   4.547 +  Outer_Syntax.local_theory_to_proof' spec
   4.548 +    ("state " ^ descr)
   4.549 +    (Scan.optional (Parse_Spec.opt_thm_name ":" --|
   4.550 +      Scan.ahead (Parse_Spec.includes >> K "" ||
   4.551 +        Parse_Spec.locale_keyword || Parse_Spec.statement_keyword)) Attrib.empty_binding --
   4.552 +      Scan.optional Parse_Spec.includes [] --
   4.553 +      Parse_Spec.general_statement >> (fn ((a, includes), (elems, concl)) =>
   4.554 +        ((if schematic then Specification.schematic_theorem_cmd else Specification.theorem_cmd)
   4.555 +          Thm.theoremK NONE (K I) a includes elems concl)));
   4.556 +
   4.557 +val _ = theorem @{command_keyword theorem} false "theorem";
   4.558 +val _ = theorem @{command_keyword lemma} false "lemma";
   4.559 +val _ = theorem @{command_keyword corollary} false "corollary";
   4.560 +val _ = theorem @{command_keyword proposition} false "proposition";
   4.561 +val _ = theorem @{command_keyword schematic_goal} true "schematic goal";
   4.562 +
   4.563 +
   4.564 +val _ =
   4.565 +  Outer_Syntax.command @{command_keyword have} "state local goal"
   4.566 +    (structured_statement >> (fn (a, b, c, d) =>
   4.567 +      Toplevel.proof' (fn int => Proof.have_cmd a NONE (K I) b c d int #> #2)));
   4.568 +
   4.569 +val _ =
   4.570 +  Outer_Syntax.command @{command_keyword show} "state local goal, to refine pending subgoals"
   4.571 +    (structured_statement >> (fn (a, b, c, d) =>
   4.572 +      Toplevel.proof' (fn int => Proof.show_cmd a NONE (K I) b c d int #> #2)));
   4.573 +
   4.574 +val _ =
   4.575 +  Outer_Syntax.command @{command_keyword hence} "old-style alias of \"then have\""
   4.576 +    (structured_statement >> (fn (a, b, c, d) =>
   4.577 +      Toplevel.proof' (fn int => Proof.chain #> Proof.have_cmd a NONE (K I) b c d int #> #2)));
   4.578 +
   4.579 +val _ =
   4.580 +  Outer_Syntax.command @{command_keyword thus} "old-style alias of  \"then show\""
   4.581 +    (structured_statement >> (fn (a, b, c, d) =>
   4.582 +      Toplevel.proof' (fn int => Proof.chain #> Proof.show_cmd a NONE (K I) b c d int #> #2)));
   4.583 +
   4.584 +
   4.585 +(* facts *)
   4.586 +
   4.587 +val facts = Parse.and_list1 Parse.xthms1;
   4.588 +
   4.589 +val _ =
   4.590 +  Outer_Syntax.command @{command_keyword then} "forward chaining"
   4.591 +    (Scan.succeed (Toplevel.proof Proof.chain));
   4.592 +
   4.593 +val _ =
   4.594 +  Outer_Syntax.command @{command_keyword from} "forward chaining from given facts"
   4.595 +    (facts >> (Toplevel.proof o Proof.from_thmss_cmd));
   4.596 +
   4.597 +val _ =
   4.598 +  Outer_Syntax.command @{command_keyword with} "forward chaining from given and current facts"
   4.599 +    (facts >> (Toplevel.proof o Proof.with_thmss_cmd));
   4.600 +
   4.601 +val _ =
   4.602 +  Outer_Syntax.command @{command_keyword note} "define facts"
   4.603 +    (Parse_Spec.name_facts >> (Toplevel.proof o Proof.note_thmss_cmd));
   4.604 +
   4.605 +val _ =
   4.606 +  Outer_Syntax.command @{command_keyword supply} "define facts during goal refinement (unstructured)"
   4.607 +    (Parse_Spec.name_facts >> (Toplevel.proof o Proof.supply_cmd));
   4.608 +
   4.609 +val _ =
   4.610 +  Outer_Syntax.command @{command_keyword using} "augment goal facts"
   4.611 +    (facts >> (Toplevel.proof o Proof.using_cmd));
   4.612 +
   4.613 +val _ =
   4.614 +  Outer_Syntax.command @{command_keyword unfolding} "unfold definitions in goal and facts"
   4.615 +    (facts >> (Toplevel.proof o Proof.unfolding_cmd));
   4.616 +
   4.617 +
   4.618 +(* proof context *)
   4.619 +
   4.620 +val _ =
   4.621 +  Outer_Syntax.command @{command_keyword fix} "fix local variables (Skolem constants)"
   4.622 +    (Parse.fixes >> (Toplevel.proof o Proof.fix_cmd));
   4.623 +
   4.624 +val _ =
   4.625 +  Outer_Syntax.command @{command_keyword assume} "assume propositions"
   4.626 +    (structured_statement' >> (fn (a, b, c) => Toplevel.proof (Proof.assume_cmd a b c)));
   4.627 +
   4.628 +val _ =
   4.629 +  Outer_Syntax.command @{command_keyword presume} "assume propositions, to be established later"
   4.630 +    (structured_statement' >> (fn (a, b, c) => Toplevel.proof (Proof.presume_cmd a b c)));
   4.631 +
   4.632 +val _ =
   4.633 +  Outer_Syntax.command @{command_keyword def} "local definition (non-polymorphic)"
   4.634 +    (Parse.and_list1
   4.635 +      (Parse_Spec.opt_thm_name ":" --
   4.636 +        ((Parse.binding -- Parse.opt_mixfix) --
   4.637 +          ((@{keyword "\<equiv>"} || @{keyword "=="}) |-- Parse.!!! Parse.termp)))
   4.638 +    >> (Toplevel.proof o Proof.def_cmd));
   4.639 +
   4.640 +val _ =
   4.641 +  Outer_Syntax.command @{command_keyword consider} "state cases rule"
   4.642 +    (Parse_Spec.obtains >> (Toplevel.proof' o Obtain.consider_cmd));
   4.643 +
   4.644 +val _ =
   4.645 +  Outer_Syntax.command @{command_keyword obtain} "generalized elimination"
   4.646 +    (Parse.parbinding -- Scan.optional (Parse.fixes --| Parse.where_) [] -- Parse_Spec.statement
   4.647 +      >> (fn ((x, y), z) => Toplevel.proof' (Obtain.obtain_cmd x y z)));
   4.648 +
   4.649 +val _ =
   4.650 +  Outer_Syntax.command @{command_keyword guess} "wild guessing (unstructured)"
   4.651 +    (Scan.optional Parse.fixes [] >> (Toplevel.proof' o Obtain.guess_cmd));
   4.652 +
   4.653 +val _ =
   4.654 +  Outer_Syntax.command @{command_keyword let} "bind text variables"
   4.655 +    (Parse.and_list1 (Parse.and_list1 Parse.term -- (@{keyword "="} |-- Parse.term))
   4.656 +      >> (Toplevel.proof o Proof.let_bind_cmd));
   4.657 +
   4.658 +val _ =
   4.659 +  Outer_Syntax.command @{command_keyword write} "add concrete syntax for constants / fixed variables"
   4.660 +    (opt_mode -- Parse.and_list1 (Parse.const -- Parse.mixfix)
   4.661 +    >> (fn (mode, args) => Toplevel.proof (Proof.write_cmd mode args)));
   4.662 +
   4.663 +val _ =
   4.664 +  Outer_Syntax.command @{command_keyword case} "invoke local context"
   4.665 +    (Parse_Spec.opt_thm_name ":" --
   4.666 +      (@{keyword "("} |--
   4.667 +        Parse.!!! (Parse.position Parse.xname -- Scan.repeat (Parse.maybe Parse.binding)
   4.668 +          --| @{keyword ")"}) ||
   4.669 +        Parse.position Parse.xname >> rpair []) >> (Toplevel.proof o Proof.case_cmd));
   4.670 +
   4.671 +
   4.672 +(* proof structure *)
   4.673 +
   4.674 +val _ =
   4.675 +  Outer_Syntax.command @{command_keyword "{"} "begin explicit proof block"
   4.676 +    (Scan.succeed (Toplevel.proof Proof.begin_block));
   4.677 +
   4.678 +val _ =
   4.679 +  Outer_Syntax.command @{command_keyword "}"} "end explicit proof block"
   4.680 +    (Scan.succeed (Toplevel.proof Proof.end_block));
   4.681 +
   4.682 +val _ =
   4.683 +  Outer_Syntax.command @{command_keyword next} "enter next proof block"
   4.684 +    (Scan.succeed (Toplevel.proof Proof.next_block));
   4.685 +
   4.686 +
   4.687 +(* end proof *)
   4.688 +
   4.689 +val _ =
   4.690 +  Outer_Syntax.command @{command_keyword qed} "conclude proof"
   4.691 +    (Scan.option Method.parse >> (fn m =>
   4.692 +     (Option.map Method.report m;
   4.693 +      Isar_Cmd.qed m)));
   4.694 +
   4.695 +val _ =
   4.696 +  Outer_Syntax.command @{command_keyword by} "terminal backward proof"
   4.697 +    (Method.parse -- Scan.option Method.parse >> (fn (m1, m2) =>
   4.698 +     (Method.report m1;
   4.699 +      Option.map Method.report m2;
   4.700 +      Isar_Cmd.terminal_proof (m1, m2))));
   4.701 +
   4.702 +val _ =
   4.703 +  Outer_Syntax.command @{command_keyword ".."} "default proof"
   4.704 +    (Scan.succeed Isar_Cmd.default_proof);
   4.705 +
   4.706 +val _ =
   4.707 +  Outer_Syntax.command @{command_keyword "."} "immediate proof"
   4.708 +    (Scan.succeed Isar_Cmd.immediate_proof);
   4.709 +
   4.710 +val _ =
   4.711 +  Outer_Syntax.command @{command_keyword done} "done proof"
   4.712 +    (Scan.succeed Isar_Cmd.done_proof);
   4.713 +
   4.714 +val _ =
   4.715 +  Outer_Syntax.command @{command_keyword sorry} "skip proof (quick-and-dirty mode only!)"
   4.716 +    (Scan.succeed Isar_Cmd.skip_proof);
   4.717 +
   4.718 +val _ =
   4.719 +  Outer_Syntax.command @{command_keyword "\<proof>"} "dummy proof (quick-and-dirty mode only!)"
   4.720 +    (Scan.succeed Isar_Cmd.skip_proof);
   4.721 +
   4.722 +val _ =
   4.723 +  Outer_Syntax.command @{command_keyword oops} "forget proof"
   4.724 +    (Scan.succeed (Toplevel.forget_proof true));
   4.725 +
   4.726 +
   4.727 +(* proof steps *)
   4.728 +
   4.729 +val _ =
   4.730 +  Outer_Syntax.command @{command_keyword defer} "shuffle internal proof state"
   4.731 +    (Scan.optional Parse.nat 1 >> (Toplevel.proof o Proof.defer));
   4.732 +
   4.733 +val _ =
   4.734 +  Outer_Syntax.command @{command_keyword prefer} "shuffle internal proof state"
   4.735 +    (Parse.nat >> (Toplevel.proof o Proof.prefer));
   4.736 +
   4.737 +val _ =
   4.738 +  Outer_Syntax.command @{command_keyword apply} "initial goal refinement step (unstructured)"
   4.739 +    (Method.parse >> (fn m => (Method.report m; Toplevel.proofs (Proof.apply m))));
   4.740 +
   4.741 +val _ =
   4.742 +  Outer_Syntax.command @{command_keyword apply_end} "terminal goal refinement step (unstructured)"
   4.743 +    (Method.parse >> (fn m => (Method.report m; Toplevel.proofs (Proof.apply_end m))));
   4.744 +
   4.745 +val _ =
   4.746 +  Outer_Syntax.command @{command_keyword proof} "backward proof step"
   4.747 +    (Scan.option Method.parse >> (fn m =>
   4.748 +      (Option.map Method.report m; Toplevel.proofs (Proof.proof m))));
   4.749 +
   4.750 +
   4.751 +(* subgoal focus *)
   4.752 +
   4.753 +local
   4.754 +
   4.755 +val opt_fact_binding =
   4.756 +  Scan.optional (Parse.binding -- Parse.opt_attribs || Parse.attribs >> pair Binding.empty)
   4.757 +    Attrib.empty_binding;
   4.758 +
   4.759 +val for_params =
   4.760 +  Scan.optional
   4.761 +    (@{keyword "for"} |--
   4.762 +      Parse.!!! ((Scan.option Parse.dots >> is_some) --
   4.763 +        (Scan.repeat1 (Parse.position (Parse.maybe Parse.name)))))
   4.764 +    (false, []);
   4.765 +
   4.766 +in
   4.767 +
   4.768 +val _ =
   4.769 +  Outer_Syntax.command @{command_keyword subgoal}
   4.770 +    "focus on first subgoal within backward refinement"
   4.771 +    (opt_fact_binding -- (Scan.option (@{keyword "premises"} |-- Parse.!!! opt_fact_binding)) --
   4.772 +      for_params >> (fn ((a, b), c) =>
   4.773 +        Toplevel.proofs (Seq.make_results o Seq.single o #2 o Subgoal.subgoal_cmd a b c)));
   4.774 +
   4.775 +end;
   4.776 +
   4.777 +
   4.778 +(* calculation *)
   4.779 +
   4.780 +val calculation_args =
   4.781 +  Scan.option (@{keyword "("} |-- Parse.!!! ((Parse.xthms1 --| @{keyword ")"})));
   4.782 +
   4.783 +val _ =
   4.784 +  Outer_Syntax.command @{command_keyword also} "combine calculation and current facts"
   4.785 +    (calculation_args >> (Toplevel.proofs' o Calculation.also_cmd));
   4.786 +
   4.787 +val _ =
   4.788 +  Outer_Syntax.command @{command_keyword finally}
   4.789 +    "combine calculation and current facts, exhibit result"
   4.790 +    (calculation_args >> (Toplevel.proofs' o Calculation.finally_cmd));
   4.791 +
   4.792 +val _ =
   4.793 +  Outer_Syntax.command @{command_keyword moreover} "augment calculation by current facts"
   4.794 +    (Scan.succeed (Toplevel.proof' Calculation.moreover));
   4.795 +
   4.796 +val _ =
   4.797 +  Outer_Syntax.command @{command_keyword ultimately}
   4.798 +    "augment calculation by current facts, exhibit result"
   4.799 +    (Scan.succeed (Toplevel.proof' Calculation.ultimately));
   4.800 +
   4.801 +val _ =
   4.802 +  Outer_Syntax.command @{command_keyword print_trans_rules} "print transitivity rules"
   4.803 +    (Scan.succeed (Toplevel.keep (Calculation.print_rules o Toplevel.context_of)));
   4.804 +
   4.805 +
   4.806 +(* proof navigation *)
   4.807 +
   4.808 +fun report_back () =
   4.809 +  Output.report [Markup.markup Markup.bad "Explicit backtracking"];
   4.810 +
   4.811 +val _ =
   4.812 +  Outer_Syntax.command @{command_keyword back} "explicit backtracking of proof command"
   4.813 +    (Scan.succeed
   4.814 +     (Toplevel.actual_proof (fn prf => (report_back (); Proof_Node.back prf)) o
   4.815 +      Toplevel.skip_proof report_back));
   4.816 +
   4.817 +
   4.818 +
   4.819 +(** diagnostic commands (for interactive mode only) **)
   4.820 +
   4.821 +val opt_modes =
   4.822 +  Scan.optional (@{keyword "("} |-- Parse.!!! (Scan.repeat1 Parse.xname --| @{keyword ")"})) [];
   4.823 +
   4.824 +val _ =
   4.825 +  Outer_Syntax.command @{command_keyword help}
   4.826 +    "retrieve outer syntax commands according to name patterns"
   4.827 +    (Scan.repeat Parse.name >>
   4.828 +      (fn pats => Toplevel.keep (fn st => Outer_Syntax.help (Toplevel.theory_of st) pats)));
   4.829 +
   4.830 +val _ =
   4.831 +  Outer_Syntax.command @{command_keyword print_commands} "print outer syntax commands"
   4.832 +    (Scan.succeed (Toplevel.keep (Outer_Syntax.print_commands o Toplevel.theory_of)));
   4.833 +
   4.834 +val _ =
   4.835 +  Outer_Syntax.command @{command_keyword print_options} "print configuration options"
   4.836 +    (Parse.opt_bang >> (fn b => Toplevel.keep (Attrib.print_options b o Toplevel.context_of)));
   4.837 +
   4.838 +val _ =
   4.839 +  Outer_Syntax.command @{command_keyword print_context}
   4.840 +    "print context of local theory target"
   4.841 +    (Scan.succeed (Toplevel.keep (Pretty.writeln_chunks o Toplevel.pretty_context)));
   4.842 +
   4.843 +val _ =
   4.844 +  Outer_Syntax.command @{command_keyword print_theory}
   4.845 +    "print logical theory contents"
   4.846 +    (Parse.opt_bang >> (fn b =>
   4.847 +      Toplevel.keep (Pretty.writeln o Proof_Display.pretty_theory b o Toplevel.context_of)));
   4.848 +
   4.849 +val _ =
   4.850 +  Outer_Syntax.command @{command_keyword print_definitions}
   4.851 +    "print dependencies of definitional theory content"
   4.852 +    (Parse.opt_bang >> (fn b =>
   4.853 +      Toplevel.keep (Pretty.writeln o Proof_Display.pretty_definitions b o Toplevel.context_of)));
   4.854 +
   4.855 +val _ =
   4.856 +  Outer_Syntax.command @{command_keyword print_syntax}
   4.857 +    "print inner syntax of context"
   4.858 +    (Scan.succeed (Toplevel.keep (Proof_Context.print_syntax o Toplevel.context_of)));
   4.859 +
   4.860 +val _ =
   4.861 +  Outer_Syntax.command @{command_keyword print_defn_rules}
   4.862 +    "print definitional rewrite rules of context"
   4.863 +    (Scan.succeed (Toplevel.keep (Local_Defs.print_rules o Toplevel.context_of)));
   4.864 +
   4.865 +val _ =
   4.866 +  Outer_Syntax.command @{command_keyword print_abbrevs}
   4.867 +    "print constant abbreviations of context"
   4.868 +    (Parse.opt_bang >> (fn b =>
   4.869 +      Toplevel.keep (Proof_Context.print_abbrevs b o Toplevel.context_of)));
   4.870 +
   4.871 +val _ =
   4.872 +  Outer_Syntax.command @{command_keyword print_theorems}
   4.873 +    "print theorems of local theory or proof context"
   4.874 +    (Parse.opt_bang >> (fn b =>
   4.875 +      Toplevel.keep (Pretty.writeln o Pretty.chunks o Isar_Cmd.pretty_theorems b)));
   4.876 +
   4.877 +val _ =
   4.878 +  Outer_Syntax.command @{command_keyword print_locales}
   4.879 +    "print locales of this theory"
   4.880 +    (Parse.opt_bang >> (fn b =>
   4.881 +      Toplevel.keep (Locale.print_locales b o Toplevel.theory_of)));
   4.882 +
   4.883 +val _ =
   4.884 +  Outer_Syntax.command @{command_keyword print_classes}
   4.885 +    "print classes of this theory"
   4.886 +    (Scan.succeed (Toplevel.keep (Class.print_classes o Toplevel.context_of)));
   4.887 +
   4.888 +val _ =
   4.889 +  Outer_Syntax.command @{command_keyword print_locale}
   4.890 +    "print locale of this theory"
   4.891 +    (Parse.opt_bang -- Parse.position Parse.xname >> (fn (b, name) =>
   4.892 +      Toplevel.keep (fn state => Locale.print_locale (Toplevel.theory_of state) b name)));
   4.893 +
   4.894 +val _ =
   4.895 +  Outer_Syntax.command @{command_keyword print_interps}
   4.896 +    "print interpretations of locale for this theory or proof context"
   4.897 +    (Parse.position Parse.xname >> (fn name =>
   4.898 +      Toplevel.keep (fn state => Locale.print_registrations (Toplevel.context_of state) name)));
   4.899 +
   4.900 +val _ =
   4.901 +  Outer_Syntax.command @{command_keyword print_dependencies}
   4.902 +    "print dependencies of locale expression"
   4.903 +    (Parse.opt_bang -- Parse_Spec.locale_expression >> (fn (b, expr) =>
   4.904 +      Toplevel.keep (fn state => Expression.print_dependencies (Toplevel.context_of state) b expr)));
   4.905 +
   4.906 +val _ =
   4.907 +  Outer_Syntax.command @{command_keyword print_attributes}
   4.908 +    "print attributes of this theory"
   4.909 +    (Parse.opt_bang >> (fn b => Toplevel.keep (Attrib.print_attributes b o Toplevel.context_of)));
   4.910 +
   4.911 +val _ =
   4.912 +  Outer_Syntax.command @{command_keyword print_simpset}
   4.913 +    "print context of Simplifier"
   4.914 +    (Parse.opt_bang >> (fn b =>
   4.915 +      Toplevel.keep (Pretty.writeln o Simplifier.pretty_simpset b o Toplevel.context_of)));
   4.916 +
   4.917 +val _ =
   4.918 +  Outer_Syntax.command @{command_keyword print_rules} "print intro/elim rules"
   4.919 +    (Scan.succeed (Toplevel.keep (Context_Rules.print_rules o Toplevel.context_of)));
   4.920 +
   4.921 +val _ =
   4.922 +  Outer_Syntax.command @{command_keyword print_methods} "print methods of this theory"
   4.923 +    (Parse.opt_bang >> (fn b => Toplevel.keep (Method.print_methods b o Toplevel.context_of)));
   4.924 +
   4.925 +val _ =
   4.926 +  Outer_Syntax.command @{command_keyword print_antiquotations}
   4.927 +    "print document antiquotations"
   4.928 +    (Parse.opt_bang >> (fn b =>
   4.929 +      Toplevel.keep (Thy_Output.print_antiquotations b o Toplevel.context_of)));
   4.930 +
   4.931 +val _ =
   4.932 +  Outer_Syntax.command @{command_keyword print_ML_antiquotations}
   4.933 +    "print ML antiquotations"
   4.934 +    (Parse.opt_bang >> (fn b =>
   4.935 +      Toplevel.keep (ML_Context.print_antiquotations b o Toplevel.context_of)));
   4.936 +
   4.937 +val _ =
   4.938 +  Outer_Syntax.command @{command_keyword locale_deps} "visualize locale dependencies"
   4.939 +    (Scan.succeed
   4.940 +      (Toplevel.keep (Toplevel.theory_of #> (fn thy =>
   4.941 +        Locale.pretty_locale_deps thy
   4.942 +        |> map (fn {name, parents, body} =>
   4.943 +          ((name, Graph_Display.content_node (Locale.extern thy name) [body]), parents))
   4.944 +        |> Graph_Display.display_graph_old))));
   4.945 +
   4.946 +val _ =
   4.947 +  Outer_Syntax.command @{command_keyword print_term_bindings}
   4.948 +    "print term bindings of proof context"
   4.949 +    (Scan.succeed
   4.950 +      (Toplevel.keep
   4.951 +        (Pretty.writeln_chunks o Proof_Context.pretty_term_bindings o Toplevel.context_of)));
   4.952 +
   4.953 +val _ =
   4.954 +  Outer_Syntax.command @{command_keyword print_facts} "print facts of proof context"
   4.955 +    (Parse.opt_bang >> (fn b =>
   4.956 +      Toplevel.keep (Proof_Context.print_local_facts b o Toplevel.context_of)));
   4.957 +
   4.958 +val _ =
   4.959 +  Outer_Syntax.command @{command_keyword print_cases} "print cases of proof context"
   4.960 +    (Scan.succeed
   4.961 +      (Toplevel.keep (Pretty.writeln_chunks o Proof_Context.pretty_cases o Toplevel.context_of)));
   4.962 +
   4.963 +val _ =
   4.964 +  Outer_Syntax.command @{command_keyword print_statement}
   4.965 +    "print theorems as long statements"
   4.966 +    (opt_modes -- Parse.xthms1 >> Isar_Cmd.print_stmts);
   4.967 +
   4.968 +val _ =
   4.969 +  Outer_Syntax.command @{command_keyword thm} "print theorems"
   4.970 +    (opt_modes -- Parse.xthms1 >> Isar_Cmd.print_thms);
   4.971 +
   4.972 +val _ =
   4.973 +  Outer_Syntax.command @{command_keyword prf} "print proof terms of theorems"
   4.974 +    (opt_modes -- Scan.option Parse.xthms1 >> Isar_Cmd.print_prfs false);
   4.975 +
   4.976 +val _ =
   4.977 +  Outer_Syntax.command @{command_keyword full_prf} "print full proof terms of theorems"
   4.978 +    (opt_modes -- Scan.option Parse.xthms1 >> Isar_Cmd.print_prfs true);
   4.979 +
   4.980 +val _ =
   4.981 +  Outer_Syntax.command @{command_keyword prop} "read and print proposition"
   4.982 +    (opt_modes -- Parse.term >> Isar_Cmd.print_prop);
   4.983 +
   4.984 +val _ =
   4.985 +  Outer_Syntax.command @{command_keyword term} "read and print term"
   4.986 +    (opt_modes -- Parse.term >> Isar_Cmd.print_term);
   4.987 +
   4.988 +val _ =
   4.989 +  Outer_Syntax.command @{command_keyword typ} "read and print type"
   4.990 +    (opt_modes -- (Parse.typ -- Scan.option (@{keyword "::"} |-- Parse.!!! Parse.sort))
   4.991 +      >> Isar_Cmd.print_type);
   4.992 +
   4.993 +val _ =
   4.994 +  Outer_Syntax.command @{command_keyword print_codesetup} "print code generator setup"
   4.995 +    (Scan.succeed (Toplevel.keep (Code.print_codesetup o Toplevel.theory_of)));
   4.996 +
   4.997 +val _ =
   4.998 +  Outer_Syntax.command @{command_keyword print_state}
   4.999 +    "print current proof state (if present)"
  4.1000 +    (opt_modes >> (fn modes =>
  4.1001 +      Toplevel.keep (Print_Mode.with_modes modes (Output.state o Toplevel.string_of_state))));
  4.1002 +
  4.1003 +val _ =
  4.1004 +  Outer_Syntax.command @{command_keyword welcome} "print welcome message"
  4.1005 +    (Scan.succeed (Toplevel.keep (fn _ => writeln (Session.welcome ()))));
  4.1006 +
  4.1007 +val _ =
  4.1008 +  Outer_Syntax.command @{command_keyword display_drafts}
  4.1009 +    "display raw source files with symbols"
  4.1010 +    (Scan.repeat1 Parse.path >> (fn names =>
  4.1011 +      Toplevel.keep (fn _ => ignore (Present.display_drafts (map Path.explode names)))));
  4.1012 +
  4.1013 +
  4.1014 +(* deps *)
  4.1015 +
  4.1016 +local
  4.1017 +  val theory_bounds =
  4.1018 +    Parse.position Parse.theory_xname >> single ||
  4.1019 +    (@{keyword "("} |-- Parse.enum "|" (Parse.position Parse.theory_xname) --| @{keyword ")"});
  4.1020 +in
  4.1021 +
  4.1022 +val _ =
  4.1023 +  Outer_Syntax.command @{command_keyword thy_deps} "visualize theory dependencies"
  4.1024 +    (Scan.option theory_bounds -- Scan.option theory_bounds >>
  4.1025 +      (fn args => Toplevel.keep (fn st => Thy_Deps.thy_deps_cmd (Toplevel.context_of st) args)));
  4.1026 +
  4.1027 +end;
  4.1028 +
  4.1029 +local
  4.1030 +  val class_bounds =
  4.1031 +    Parse.sort >> single ||
  4.1032 +    (@{keyword "("} |-- Parse.enum "|" Parse.sort --| @{keyword ")"});
  4.1033 +in
  4.1034 +
  4.1035 +val _ =
  4.1036 +  Outer_Syntax.command @{command_keyword class_deps} "visualize class dependencies"
  4.1037 +    (Scan.option class_bounds -- Scan.option class_bounds >> (fn args =>
  4.1038 +      Toplevel.keep (fn st => Class_Deps.class_deps_cmd (Toplevel.context_of st) args)));
  4.1039 +
  4.1040 +end;
  4.1041 +
  4.1042 +val _ =
  4.1043 +  Outer_Syntax.command @{command_keyword thm_deps} "visualize theorem dependencies"
  4.1044 +    (Parse.xthms1 >> (fn args =>
  4.1045 +      Toplevel.keep (fn st =>
  4.1046 +        Thm_Deps.thm_deps (Toplevel.theory_of st)
  4.1047 +          (Attrib.eval_thms (Toplevel.context_of st) args))));
  4.1048 +
  4.1049 +local
  4.1050 +  val thy_names =
  4.1051 +    Scan.repeat1 (Scan.unless Parse.minus (Parse.position Parse.theory_xname));
  4.1052 +in
  4.1053 +
  4.1054 +val _ =
  4.1055 +  Outer_Syntax.command @{command_keyword unused_thms} "find unused theorems"
  4.1056 +    (Scan.option ((thy_names --| Parse.minus) -- Scan.option thy_names) >> (fn opt_range =>
  4.1057 +        Toplevel.keep (fn st =>
  4.1058 +          let
  4.1059 +            val thy = Toplevel.theory_of st;
  4.1060 +            val ctxt = Toplevel.context_of st;
  4.1061 +            fun pretty_thm (a, th) = Proof_Context.pretty_fact ctxt (a, [th]);
  4.1062 +            val check = Theory.check ctxt;
  4.1063 +          in
  4.1064 +            Thm_Deps.unused_thms
  4.1065 +              (case opt_range of
  4.1066 +                NONE => (Theory.parents_of thy, [thy])
  4.1067 +              | SOME (xs, NONE) => (map check xs, [thy])
  4.1068 +              | SOME (xs, SOME ys) => (map check xs, map check ys))
  4.1069 +            |> map pretty_thm |> Pretty.writeln_chunks
  4.1070 +          end)));
  4.1071 +
  4.1072 +end;
  4.1073 +
  4.1074 +
  4.1075 +(* find *)
  4.1076 +
  4.1077 +val _ =
  4.1078 +  Outer_Syntax.command @{command_keyword find_consts}
  4.1079 +    "find constants by name / type patterns"
  4.1080 +    (Find_Consts.query_parser >> (fn spec =>
  4.1081 +      Toplevel.keep (fn st =>
  4.1082 +        Pretty.writeln (Find_Consts.pretty_consts (Toplevel.context_of st) spec))));
  4.1083 +
  4.1084 +local
  4.1085 +  val options =
  4.1086 +    Scan.optional
  4.1087 +      (Parse.$$$ "(" |--
  4.1088 +        Parse.!!! (Scan.option Parse.nat --
  4.1089 +          Scan.optional (Parse.reserved "with_dups" >> K false) true --| Parse.$$$ ")"))
  4.1090 +      (NONE, true);
  4.1091 +in
  4.1092 +
  4.1093 +val _ =
  4.1094 +  Outer_Syntax.command @{command_keyword find_theorems}
  4.1095 +    "find theorems meeting specified criteria"
  4.1096 +    (options -- Find_Theorems.query_parser >> (fn ((opt_lim, rem_dups), spec) =>
  4.1097 +      Toplevel.keep (fn st =>
  4.1098 +        Pretty.writeln
  4.1099 +          (Find_Theorems.pretty_theorems (Find_Theorems.proof_state st) opt_lim rem_dups spec))));
  4.1100 +
  4.1101 +end;
  4.1102 +
  4.1103 +
  4.1104 +
  4.1105 +(** extraction of programs from proofs **)
  4.1106 +
  4.1107 +val parse_vars = Scan.optional (Parse.$$$ "(" |-- Parse.list1 Parse.name --| Parse.$$$ ")") [];
  4.1108 +
  4.1109 +val _ =
  4.1110 +  Outer_Syntax.command @{command_keyword realizers}
  4.1111 +    "specify realizers for primitive axioms / theorems, together with correctness proof"
  4.1112 +    (Scan.repeat1 (Parse.xname -- parse_vars --| Parse.$$$ ":" -- Parse.string -- Parse.string) >>
  4.1113 +     (fn xs => Toplevel.theory (fn thy => Extraction.add_realizers
  4.1114 +       (map (fn (((a, vs), s1), s2) => (Global_Theory.get_thm thy a, (vs, s1, s2))) xs) thy)));
  4.1115 +
  4.1116 +val _ =
  4.1117 +  Outer_Syntax.command @{command_keyword realizability}
  4.1118 +    "add equations characterizing realizability"
  4.1119 +    (Scan.repeat1 Parse.string >> (Toplevel.theory o Extraction.add_realizes_eqns));
  4.1120 +
  4.1121 +val _ =
  4.1122 +  Outer_Syntax.command @{command_keyword extract_type}
  4.1123 +    "add equations characterizing type of extracted program"
  4.1124 +    (Scan.repeat1 Parse.string >> (Toplevel.theory o Extraction.add_typeof_eqns));
  4.1125 +
  4.1126 +val _ =
  4.1127 +  Outer_Syntax.command @{command_keyword extract} "extract terms from proofs"
  4.1128 +    (Scan.repeat1 (Parse.xname -- parse_vars) >> (fn xs => Toplevel.theory (fn thy =>
  4.1129 +      Extraction.extract (map (apfst (Global_Theory.get_thm thy)) xs) thy)));
  4.1130 +
  4.1131 +
  4.1132 +
  4.1133 +(** end **)
  4.1134 +
  4.1135 +val _ =
  4.1136 +  Outer_Syntax.command @{command_keyword end} "end context"
  4.1137 +    (Scan.succeed
  4.1138 +      (Toplevel.exit o Toplevel.end_local_theory o Toplevel.close_target o
  4.1139 +        Toplevel.end_proof (K Proof.end_notepad)));
  4.1140 +
  4.1141 +in end;
  4.1142 +\<close>
  4.1143  
  4.1144  
  4.1145  section \<open>Basic attributes\<close>
     5.1 --- a/src/Pure/ROOT	Mon Apr 04 17:02:34 2016 +0200
     5.2 +++ b/src/Pure/ROOT	Mon Apr 04 17:25:53 2016 +0200
     5.3 @@ -108,7 +108,6 @@
     5.4      "ML/ml_context.ML"
     5.5      "ML/ml_debugger.ML"
     5.6      "ML/ml_env.ML"
     5.7 -    "ML/ml_file.ML"
     5.8      "ML/ml_final.ML"
     5.9      "ML/ml_heap.ML"
    5.10      "ML/ml_lex.ML"
     6.1 --- a/src/Pure/ROOT.ML	Mon Apr 04 17:02:34 2016 +0200
     6.2 +++ b/src/Pure/ROOT.ML	Mon Apr 04 17:25:53 2016 +0200
     6.3 @@ -318,14 +318,13 @@
     6.4  
     6.5  (* miscellaneous tools and packages for Pure Isabelle *)
     6.6  
     6.7 +use "ML/ml_pp.ML";
     6.8 +use "ML/ml_antiquotations.ML";
     6.9 +use "ML/ml_thms.ML";
    6.10 +
    6.11  use "Tools/build.ML";
    6.12  use "Tools/named_thms.ML";
    6.13 -use "ML/ml_pp.ML";
    6.14 -use "ML/ml_file.ML";
    6.15 -use "ML/ml_antiquotations.ML";
    6.16 -use "ML/ml_thms.ML";
    6.17  use "Tools/print_operation.ML";
    6.18 -
    6.19  use "Tools/bibtex.ML";
    6.20  use "Tools/rail.ML";
    6.21  use "Tools/rule_insts.ML";
     7.1 --- a/src/Pure/Thy/thy_header.ML	Mon Apr 04 17:02:34 2016 +0200
     7.2 +++ b/src/Pure/Thy/thy_header.ML	Mon Apr 04 17:25:53 2016 +0200
     7.3 @@ -80,9 +80,7 @@
     7.4       ((txtN, @{here}), SOME ((Keyword.document_body, []), [])),
     7.5       ((text_rawN, @{here}), SOME ((Keyword.document_raw, []), [])),
     7.6       ((theoryN, @{here}), SOME ((Keyword.thy_begin, []), ["theory"])),
     7.7 -     (("ML_file", @{here}), SOME ((Keyword.thy_load, []), ["ML"])),
     7.8 -     (("ML_file_debug", @{here}), SOME ((Keyword.thy_load, []), ["ML"])),
     7.9 -     (("ML_file_no_debug", @{here}), SOME ((Keyword.thy_load, []), ["ML"]))];
    7.10 +     (("ML", @{here}), SOME ((Keyword.thy_decl, []), ["ML"]))];
    7.11  
    7.12  
    7.13  (* theory data *)
     8.1 --- a/src/Pure/Thy/thy_header.scala	Mon Apr 04 17:02:34 2016 +0200
     8.2 +++ b/src/Pure/Thy/thy_header.scala	Mon Apr 04 17:25:53 2016 +0200
     8.3 @@ -57,9 +57,7 @@
     8.4        (TXT, Some(((Keyword.DOCUMENT_BODY, Nil), Nil)), None),
     8.5        (TEXT_RAW, Some(((Keyword.DOCUMENT_RAW, Nil), Nil)), None),
     8.6        (THEORY, Some((Keyword.THY_BEGIN, Nil), List("theory")), None),
     8.7 -      ("ML_file", Some((Keyword.THY_LOAD, Nil), List("ML")), None),
     8.8 -      ("ML_file_debug", Some((Keyword.THY_LOAD, Nil), List("ML")), None),
     8.9 -      ("ML_file_no_debug", Some((Keyword.THY_LOAD, Nil), List("ML")), None))
    8.10 +      ("ML", Some((Keyword.THY_DECL, Nil), List("ML")), None))
    8.11  
    8.12    private val bootstrap_keywords =
    8.13      Keyword.Keywords.empty.add_keywords(bootstrap_header)