tuned -- more explicit sections;
authorwenzelm
Mon Apr 04 22:13:08 2016 +0200 (2016-04-04)
changeset 628563f97aa4580c6
parent 62855 82859dac5f59
child 62857 a8758f47f9e8
tuned -- more explicit sections;
src/Pure/Isar/parse.ML
src/Pure/Pure.thy
     1.1 --- a/src/Pure/Isar/parse.ML	Mon Apr 04 20:46:39 2016 +0200
     1.2 +++ b/src/Pure/Isar/parse.ML	Mon Apr 04 22:13:08 2016 +0200
     1.3 @@ -85,6 +85,7 @@
     1.4    val mixfix': mixfix parser
     1.5    val opt_mixfix: mixfix parser
     1.6    val opt_mixfix': mixfix parser
     1.7 +  val syntax_mode: Syntax.mode parser
     1.8    val where_: string parser
     1.9    val const_decl: (string * string * mixfix) parser
    1.10    val const_binding: (binding * string * mixfix) parser
    1.11 @@ -356,6 +357,15 @@
    1.12  end;
    1.13  
    1.14  
    1.15 +(* syntax mode *)
    1.16 +
    1.17 +val syntax_mode_spec =
    1.18 +  ($$$ "output" >> K ("", false)) || name -- Scan.optional ($$$ "output" >> K false) true;
    1.19 +
    1.20 +val syntax_mode =
    1.21 +  Scan.optional ($$$ "(" |-- !!! (syntax_mode_spec --| $$$ ")")) Syntax.mode_default;
    1.22 +
    1.23 +
    1.24  (* fixes *)
    1.25  
    1.26  val where_ = $$$ "where";
     2.1 --- a/src/Pure/Pure.thy	Mon Apr 04 20:46:39 2016 +0200
     2.2 +++ b/src/Pure/Pure.thy	Mon Apr 04 22:13:08 2016 +0200
     2.3 @@ -95,191 +95,9 @@
     2.4  
     2.5  section \<open>Isar commands\<close>
     2.6  
     2.7 -ML \<open>
     2.8 -local
     2.9 -
    2.10 -(** theory commands **)
    2.11 -
    2.12 -(* sorts *)
    2.13 -
    2.14 -val _ =
    2.15 -  Outer_Syntax.local_theory @{command_keyword default_sort}
    2.16 -    "declare default sort for explicit type variables"
    2.17 -    (Parse.sort >> (fn s => fn lthy => Local_Theory.set_defsort (Syntax.read_sort lthy s) lthy));
    2.18 -
    2.19 -
    2.20 -(* types *)
    2.21 -
    2.22 -val _ =
    2.23 -  Outer_Syntax.local_theory @{command_keyword typedecl} "type declaration"
    2.24 -    (Parse.type_args -- Parse.binding -- Parse.opt_mixfix
    2.25 -      >> (fn ((args, a), mx) =>
    2.26 -          Typedecl.typedecl {final = true} (a, map (rpair dummyS) args, mx) #> snd));
    2.27 -
    2.28 -val _ =
    2.29 -  Outer_Syntax.local_theory @{command_keyword type_synonym} "declare type abbreviation"
    2.30 -    (Parse.type_args -- Parse.binding --
    2.31 -      (@{keyword "="} |-- Parse.!!! (Parse.typ -- Parse.opt_mixfix'))
    2.32 -      >> (fn ((args, a), (rhs, mx)) => snd o Typedecl.abbrev_cmd (a, args, mx) rhs));
    2.33 -
    2.34 -val _ =
    2.35 -  Outer_Syntax.command @{command_keyword nonterminal}
    2.36 -    "declare syntactic type constructors (grammar nonterminal symbols)"
    2.37 -    (Parse.and_list1 Parse.binding >> (Toplevel.theory o Sign.add_nonterminals_global));
    2.38 -
    2.39 -
    2.40 -(* consts and syntax *)
    2.41 -
    2.42 -val _ =
    2.43 -  Outer_Syntax.command @{command_keyword judgment} "declare object-logic judgment"
    2.44 -    (Parse.const_binding >> (Toplevel.theory o Object_Logic.add_judgment_cmd));
    2.45 -
    2.46 -val _ =
    2.47 -  Outer_Syntax.command @{command_keyword consts} "declare constants"
    2.48 -    (Scan.repeat1 Parse.const_binding >> (Toplevel.theory o Sign.add_consts_cmd));
    2.49 -
    2.50 -val mode_spec =
    2.51 -  (@{keyword "output"} >> K ("", false)) ||
    2.52 -    Parse.name -- Scan.optional (@{keyword "output"} >> K false) true;
    2.53 -
    2.54 -val opt_mode =
    2.55 -  Scan.optional (@{keyword "("} |-- Parse.!!! (mode_spec --| @{keyword ")"})) Syntax.mode_default;
    2.56 -
    2.57 -val _ =
    2.58 -  Outer_Syntax.command @{command_keyword syntax} "add raw syntax clauses"
    2.59 -    (opt_mode -- Scan.repeat1 Parse.const_decl
    2.60 -      >> (Toplevel.theory o uncurry Sign.add_syntax_cmd));
    2.61 -
    2.62 -val _ =
    2.63 -  Outer_Syntax.command @{command_keyword no_syntax} "delete raw syntax clauses"
    2.64 -    (opt_mode -- Scan.repeat1 Parse.const_decl
    2.65 -      >> (Toplevel.theory o uncurry Sign.del_syntax_cmd));
    2.66 -
    2.67 -
    2.68 -(* translations *)
    2.69 -
    2.70 -val trans_pat =
    2.71 -  Scan.optional
    2.72 -    (@{keyword "("} |-- Parse.!!! (Parse.inner_syntax Parse.xname --| @{keyword ")"})) "logic"
    2.73 -    -- Parse.inner_syntax Parse.string;
    2.74 -
    2.75 -fun trans_arrow toks =
    2.76 -  ((@{keyword "\<rightharpoonup>"} || @{keyword "=>"}) >> K Syntax.Parse_Rule ||
    2.77 -    (@{keyword "\<leftharpoondown>"} || @{keyword "<="}) >> K Syntax.Print_Rule ||
    2.78 -    (@{keyword "\<rightleftharpoons>"} || @{keyword "=="}) >> K Syntax.Parse_Print_Rule) toks;
    2.79 -
    2.80 -val trans_line =
    2.81 -  trans_pat -- Parse.!!! (trans_arrow -- trans_pat)
    2.82 -    >> (fn (left, (arr, right)) => arr (left, right));
    2.83 -
    2.84 -val _ =
    2.85 -  Outer_Syntax.command @{command_keyword translations} "add syntax translation rules"
    2.86 -    (Scan.repeat1 trans_line >> (Toplevel.theory o Isar_Cmd.translations));
    2.87 -
    2.88 -val _ =
    2.89 -  Outer_Syntax.command @{command_keyword no_translations} "delete syntax translation rules"
    2.90 -    (Scan.repeat1 trans_line >> (Toplevel.theory o Isar_Cmd.no_translations));
    2.91 -
    2.92 -
    2.93 -(* constant definitions and abbreviations *)
    2.94 -
    2.95 -val _ =
    2.96 -  Outer_Syntax.local_theory' @{command_keyword definition} "constant definition"
    2.97 -    (Parse_Spec.constdef >> (fn args => #2 oo Specification.definition_cmd args));
    2.98 +subsection \<open>Embedded ML text\<close>
    2.99  
   2.100 -val _ =
   2.101 -  Outer_Syntax.local_theory' @{command_keyword abbreviation} "constant abbreviation"
   2.102 -    (opt_mode -- (Scan.option Parse_Spec.constdecl -- Parse.prop)
   2.103 -      >> (fn (mode, args) => Specification.abbreviation_cmd mode args));
   2.104 -
   2.105 -val _ =
   2.106 -  Outer_Syntax.local_theory @{command_keyword type_notation}
   2.107 -    "add concrete syntax for type constructors"
   2.108 -    (opt_mode -- Parse.and_list1 (Parse.type_const -- Parse.mixfix)
   2.109 -      >> (fn (mode, args) => Specification.type_notation_cmd true mode args));
   2.110 -
   2.111 -val _ =
   2.112 -  Outer_Syntax.local_theory @{command_keyword no_type_notation}
   2.113 -    "delete concrete syntax for type constructors"
   2.114 -    (opt_mode -- Parse.and_list1 (Parse.type_const -- Parse.mixfix)
   2.115 -      >> (fn (mode, args) => Specification.type_notation_cmd false mode args));
   2.116 -
   2.117 -val _ =
   2.118 -  Outer_Syntax.local_theory @{command_keyword notation}
   2.119 -    "add concrete syntax for constants / fixed variables"
   2.120 -    (opt_mode -- Parse.and_list1 (Parse.const -- Parse.mixfix)
   2.121 -      >> (fn (mode, args) => Specification.notation_cmd true mode args));
   2.122 -
   2.123 -val _ =
   2.124 -  Outer_Syntax.local_theory @{command_keyword no_notation}
   2.125 -    "delete concrete syntax for constants / fixed variables"
   2.126 -    (opt_mode -- Parse.and_list1 (Parse.const -- Parse.mixfix)
   2.127 -      >> (fn (mode, args) => Specification.notation_cmd false mode args));
   2.128 -
   2.129 -
   2.130 -(* constant specifications *)
   2.131 -
   2.132 -val _ =
   2.133 -  Outer_Syntax.command @{command_keyword axiomatization} "axiomatic constant specification"
   2.134 -    (Scan.optional Parse.fixes [] --
   2.135 -      Scan.optional (Parse.where_ |-- Parse.!!! (Parse.and_list1 Parse_Spec.specs)) []
   2.136 -      >> (fn (x, y) => Toplevel.theory (#2 o Specification.axiomatization_cmd x y)));
   2.137 -
   2.138 -
   2.139 -(* theorems *)
   2.140 -
   2.141 -val _ =
   2.142 -  Outer_Syntax.local_theory' @{command_keyword lemmas} "define theorems"
   2.143 -    (Parse_Spec.name_facts -- Parse.for_fixes >>
   2.144 -      (fn (facts, fixes) => #2 oo Specification.theorems_cmd Thm.theoremK facts fixes));
   2.145 -
   2.146 -val _ =
   2.147 -  Outer_Syntax.local_theory' @{command_keyword declare} "declare theorems"
   2.148 -    (Parse.and_list1 Parse.xthms1 -- Parse.for_fixes
   2.149 -      >> (fn (facts, fixes) =>
   2.150 -          #2 oo Specification.theorems_cmd "" [(Attrib.empty_binding, flat facts)] fixes));
   2.151 -
   2.152 -val _ =
   2.153 -  Outer_Syntax.local_theory @{command_keyword named_theorems}
   2.154 -    "declare named collection of theorems"
   2.155 -    (Parse.and_list1 (Parse.binding -- Scan.optional Parse.text "") >>
   2.156 -      fold (fn (b, descr) => snd o Named_Theorems.declare b descr));
   2.157 -
   2.158 -
   2.159 -(* hide names *)
   2.160 -
   2.161 -local
   2.162 -
   2.163 -fun hide_names command_keyword what hide parse prep =
   2.164 -  Outer_Syntax.command command_keyword ("hide " ^ what ^ " from name space")
   2.165 -    ((Parse.opt_keyword "open" >> not) -- Scan.repeat1 parse >> (fn (fully, args) =>
   2.166 -      (Toplevel.theory (fn thy =>
   2.167 -        let val ctxt = Proof_Context.init_global thy
   2.168 -        in fold (hide fully o prep ctxt) args thy end))));
   2.169 -
   2.170 -in
   2.171 -
   2.172 -val _ =
   2.173 -  hide_names @{command_keyword hide_class} "classes" Sign.hide_class Parse.class
   2.174 -    Proof_Context.read_class;
   2.175 -
   2.176 -val _ =
   2.177 -  hide_names @{command_keyword hide_type} "types" Sign.hide_type Parse.type_const
   2.178 -    ((#1 o dest_Type) oo Proof_Context.read_type_name {proper = true, strict = false});
   2.179 -
   2.180 -val _ =
   2.181 -  hide_names @{command_keyword hide_const} "consts" Sign.hide_const Parse.const
   2.182 -    ((#1 o dest_Const) oo Proof_Context.read_const {proper = true, strict = false});
   2.183 -
   2.184 -val _ =
   2.185 -  hide_names @{command_keyword hide_fact} "facts" Global_Theory.hide_fact
   2.186 -    (Parse.position Parse.xname) (Global_Theory.check_fact o Proof_Context.theory_of);
   2.187 -
   2.188 -end;
   2.189 -
   2.190 -
   2.191 -(* use ML text *)
   2.192 -
   2.193 +ML \<open>
   2.194  local
   2.195  
   2.196  fun ML_file_cmd debug files = Toplevel.generic_theory (fn gthy =>
   2.197 @@ -309,8 +127,6 @@
   2.198        (ML_Context.exec (fn () => ML_Context.eval_source flags source))
   2.199    end);
   2.200  
   2.201 -in
   2.202 -
   2.203  val _ =
   2.204    Outer_Syntax.command ("ML_file", @{here}) "read and evaluate Isabelle/ML file"
   2.205      (Resources.parse_files "ML_file" >> ML_file_cmd NONE);
   2.206 @@ -339,8 +155,6 @@
   2.207      "read and evaluate Standard ML file (no debugger information)"
   2.208      (Resources.provide_parse_files "SML_file_no_debug" >> SML_file_cmd (SOME false));
   2.209  
   2.210 -end;
   2.211 -
   2.212  val _ =
   2.213    Outer_Syntax.command @{command_keyword SML_export} "evaluate SML within Isabelle/ML environment"
   2.214      (Parse.ML_source >> (fn source =>
   2.215 @@ -391,6 +205,11 @@
   2.216      (Parse.ML_source >> Isar_Cmd.local_setup);
   2.217  
   2.218  val _ =
   2.219 +  Outer_Syntax.command @{command_keyword oracle} "declare oracle"
   2.220 +    (Parse.range Parse.name -- (@{keyword "="} |-- Parse.ML_source) >>
   2.221 +      (fn (x, y) => Toplevel.theory (Isar_Cmd.oracle x y)));
   2.222 +
   2.223 +val _ =
   2.224    Outer_Syntax.local_theory @{command_keyword attribute_setup} "define attribute in ML"
   2.225      (Parse.position Parse.name --
   2.226          Parse.!!! (@{keyword "="} |-- Parse.ML_source -- Scan.optional Parse.text "")
   2.227 @@ -419,8 +238,101 @@
   2.228        Parse.ML_source -- Scan.optional (@{keyword "identifier"} |-- Scan.repeat1 Parse.xname) []
   2.229      >> (fn (((a, b), c), d) => Isar_Cmd.simproc_setup a b c d));
   2.230  
   2.231 +in end\<close>
   2.232  
   2.233 -(* translation functions *)
   2.234 +
   2.235 +subsection \<open>Theory commands\<close>
   2.236 +
   2.237 +subsubsection \<open>Sorts and types\<close>
   2.238 +
   2.239 +ML \<open>
   2.240 +local
   2.241 +
   2.242 +val _ =
   2.243 +  Outer_Syntax.local_theory @{command_keyword default_sort}
   2.244 +    "declare default sort for explicit type variables"
   2.245 +    (Parse.sort >> (fn s => fn lthy => Local_Theory.set_defsort (Syntax.read_sort lthy s) lthy));
   2.246 +
   2.247 +val _ =
   2.248 +  Outer_Syntax.local_theory @{command_keyword typedecl} "type declaration"
   2.249 +    (Parse.type_args -- Parse.binding -- Parse.opt_mixfix
   2.250 +      >> (fn ((args, a), mx) =>
   2.251 +          Typedecl.typedecl {final = true} (a, map (rpair dummyS) args, mx) #> snd));
   2.252 +
   2.253 +val _ =
   2.254 +  Outer_Syntax.local_theory @{command_keyword type_synonym} "declare type abbreviation"
   2.255 +    (Parse.type_args -- Parse.binding --
   2.256 +      (@{keyword "="} |-- Parse.!!! (Parse.typ -- Parse.opt_mixfix'))
   2.257 +      >> (fn ((args, a), (rhs, mx)) => snd o Typedecl.abbrev_cmd (a, args, mx) rhs));
   2.258 +
   2.259 +in end\<close>
   2.260 +
   2.261 +
   2.262 +subsubsection \<open>Consts\<close>
   2.263 +
   2.264 +ML \<open>
   2.265 +local
   2.266 +
   2.267 +val _ =
   2.268 +  Outer_Syntax.command @{command_keyword judgment} "declare object-logic judgment"
   2.269 +    (Parse.const_binding >> (Toplevel.theory o Object_Logic.add_judgment_cmd));
   2.270 +
   2.271 +val _ =
   2.272 +  Outer_Syntax.command @{command_keyword consts} "declare constants"
   2.273 +    (Scan.repeat1 Parse.const_binding >> (Toplevel.theory o Sign.add_consts_cmd));
   2.274 +
   2.275 +in end\<close>
   2.276 +
   2.277 +
   2.278 +subsubsection \<open>Syntax and translations\<close>
   2.279 +
   2.280 +ML \<open>
   2.281 +local
   2.282 +
   2.283 +val _ =
   2.284 +  Outer_Syntax.command @{command_keyword nonterminal}
   2.285 +    "declare syntactic type constructors (grammar nonterminal symbols)"
   2.286 +    (Parse.and_list1 Parse.binding >> (Toplevel.theory o Sign.add_nonterminals_global));
   2.287 +
   2.288 +val _ =
   2.289 +  Outer_Syntax.command @{command_keyword syntax} "add raw syntax clauses"
   2.290 +    (Parse.syntax_mode -- Scan.repeat1 Parse.const_decl
   2.291 +      >> (Toplevel.theory o uncurry Sign.add_syntax_cmd));
   2.292 +
   2.293 +val _ =
   2.294 +  Outer_Syntax.command @{command_keyword no_syntax} "delete raw syntax clauses"
   2.295 +    (Parse.syntax_mode -- Scan.repeat1 Parse.const_decl
   2.296 +      >> (Toplevel.theory o uncurry Sign.del_syntax_cmd));
   2.297 +
   2.298 +val trans_pat =
   2.299 +  Scan.optional
   2.300 +    (@{keyword "("} |-- Parse.!!! (Parse.inner_syntax Parse.xname --| @{keyword ")"})) "logic"
   2.301 +    -- Parse.inner_syntax Parse.string;
   2.302 +
   2.303 +fun trans_arrow toks =
   2.304 +  ((@{keyword "\<rightharpoonup>"} || @{keyword "=>"}) >> K Syntax.Parse_Rule ||
   2.305 +    (@{keyword "\<leftharpoondown>"} || @{keyword "<="}) >> K Syntax.Print_Rule ||
   2.306 +    (@{keyword "\<rightleftharpoons>"} || @{keyword "=="}) >> K Syntax.Parse_Print_Rule) toks;
   2.307 +
   2.308 +val trans_line =
   2.309 +  trans_pat -- Parse.!!! (trans_arrow -- trans_pat)
   2.310 +    >> (fn (left, (arr, right)) => arr (left, right));
   2.311 +
   2.312 +val _ =
   2.313 +  Outer_Syntax.command @{command_keyword translations} "add syntax translation rules"
   2.314 +    (Scan.repeat1 trans_line >> (Toplevel.theory o Isar_Cmd.translations));
   2.315 +
   2.316 +val _ =
   2.317 +  Outer_Syntax.command @{command_keyword no_translations} "delete syntax translation rules"
   2.318 +    (Scan.repeat1 trans_line >> (Toplevel.theory o Isar_Cmd.no_translations));
   2.319 +
   2.320 +in end\<close>
   2.321 +
   2.322 +
   2.323 +subsubsection \<open>Translation functions\<close>
   2.324 +
   2.325 +ML \<open>
   2.326 +local
   2.327  
   2.328  val _ =
   2.329    Outer_Syntax.command @{command_keyword parse_ast_translation}
   2.330 @@ -447,16 +359,124 @@
   2.331      "install print ast translation functions"
   2.332      (Parse.ML_source >> (Toplevel.theory o Isar_Cmd.print_ast_translation));
   2.333  
   2.334 +in end\<close>
   2.335  
   2.336 -(* oracles *)
   2.337 +
   2.338 +subsubsection \<open>Specifications\<close>
   2.339 +
   2.340 +ML \<open>
   2.341 +local
   2.342 +
   2.343 +val _ =
   2.344 +  Outer_Syntax.local_theory' @{command_keyword definition} "constant definition"
   2.345 +    (Parse_Spec.constdef >> (fn args => #2 oo Specification.definition_cmd args));
   2.346 +
   2.347 +val _ =
   2.348 +  Outer_Syntax.local_theory' @{command_keyword abbreviation} "constant abbreviation"
   2.349 +    (Parse.syntax_mode -- (Scan.option Parse_Spec.constdecl -- Parse.prop)
   2.350 +      >> (fn (mode, args) => Specification.abbreviation_cmd mode args));
   2.351 +
   2.352 +val _ =
   2.353 +  Outer_Syntax.command @{command_keyword axiomatization} "axiomatic constant specification"
   2.354 +    (Scan.optional Parse.fixes [] --
   2.355 +      Scan.optional (Parse.where_ |-- Parse.!!! (Parse.and_list1 Parse_Spec.specs)) []
   2.356 +      >> (fn (x, y) => Toplevel.theory (#2 o Specification.axiomatization_cmd x y)));
   2.357 +
   2.358 +in end\<close>
   2.359 +
   2.360 +
   2.361 +subsubsection \<open>Notation\<close>
   2.362 +
   2.363 +ML \<open>
   2.364 +local
   2.365 +
   2.366 +val _ =
   2.367 +  Outer_Syntax.local_theory @{command_keyword type_notation}
   2.368 +    "add concrete syntax for type constructors"
   2.369 +    (Parse.syntax_mode -- Parse.and_list1 (Parse.type_const -- Parse.mixfix)
   2.370 +      >> (fn (mode, args) => Specification.type_notation_cmd true mode args));
   2.371 +
   2.372 +val _ =
   2.373 +  Outer_Syntax.local_theory @{command_keyword no_type_notation}
   2.374 +    "delete concrete syntax for type constructors"
   2.375 +    (Parse.syntax_mode -- Parse.and_list1 (Parse.type_const -- Parse.mixfix)
   2.376 +      >> (fn (mode, args) => Specification.type_notation_cmd false mode args));
   2.377 +
   2.378 +val _ =
   2.379 +  Outer_Syntax.local_theory @{command_keyword notation}
   2.380 +    "add concrete syntax for constants / fixed variables"
   2.381 +    (Parse.syntax_mode -- Parse.and_list1 (Parse.const -- Parse.mixfix)
   2.382 +      >> (fn (mode, args) => Specification.notation_cmd true mode args));
   2.383  
   2.384  val _ =
   2.385 -  Outer_Syntax.command @{command_keyword oracle} "declare oracle"
   2.386 -    (Parse.range Parse.name -- (@{keyword "="} |-- Parse.ML_source) >>
   2.387 -      (fn (x, y) => Toplevel.theory (Isar_Cmd.oracle x y)));
   2.388 +  Outer_Syntax.local_theory @{command_keyword no_notation}
   2.389 +    "delete concrete syntax for constants / fixed variables"
   2.390 +    (Parse.syntax_mode -- Parse.and_list1 (Parse.const -- Parse.mixfix)
   2.391 +      >> (fn (mode, args) => Specification.notation_cmd false mode args));
   2.392 +
   2.393 +in end\<close>
   2.394 +
   2.395 +
   2.396 +subsubsection \<open>Theorems\<close>
   2.397 +
   2.398 +ML \<open>
   2.399 +local
   2.400 +
   2.401 +val _ =
   2.402 +  Outer_Syntax.local_theory' @{command_keyword lemmas} "define theorems"
   2.403 +    (Parse_Spec.name_facts -- Parse.for_fixes >>
   2.404 +      (fn (facts, fixes) => #2 oo Specification.theorems_cmd Thm.theoremK facts fixes));
   2.405 +
   2.406 +val _ =
   2.407 +  Outer_Syntax.local_theory' @{command_keyword declare} "declare theorems"
   2.408 +    (Parse.and_list1 Parse.xthms1 -- Parse.for_fixes
   2.409 +      >> (fn (facts, fixes) =>
   2.410 +          #2 oo Specification.theorems_cmd "" [(Attrib.empty_binding, flat facts)] fixes));
   2.411 +
   2.412 +val _ =
   2.413 +  Outer_Syntax.local_theory @{command_keyword named_theorems}
   2.414 +    "declare named collection of theorems"
   2.415 +    (Parse.and_list1 (Parse.binding -- Scan.optional Parse.text "") >>
   2.416 +      fold (fn (b, descr) => snd o Named_Theorems.declare b descr));
   2.417 +
   2.418 +in end\<close>
   2.419  
   2.420  
   2.421 -(* bundled declarations *)
   2.422 +subsubsection \<open>Hide names\<close>
   2.423 +
   2.424 +ML \<open>
   2.425 +local
   2.426 +
   2.427 +fun hide_names command_keyword what hide parse prep =
   2.428 +  Outer_Syntax.command command_keyword ("hide " ^ what ^ " from name space")
   2.429 +    ((Parse.opt_keyword "open" >> not) -- Scan.repeat1 parse >> (fn (fully, args) =>
   2.430 +      (Toplevel.theory (fn thy =>
   2.431 +        let val ctxt = Proof_Context.init_global thy
   2.432 +        in fold (hide fully o prep ctxt) args thy end))));
   2.433 +
   2.434 +val _ =
   2.435 +  hide_names @{command_keyword hide_class} "classes" Sign.hide_class Parse.class
   2.436 +    Proof_Context.read_class;
   2.437 +
   2.438 +val _ =
   2.439 +  hide_names @{command_keyword hide_type} "types" Sign.hide_type Parse.type_const
   2.440 +    ((#1 o dest_Type) oo Proof_Context.read_type_name {proper = true, strict = false});
   2.441 +
   2.442 +val _ =
   2.443 +  hide_names @{command_keyword hide_const} "consts" Sign.hide_const Parse.const
   2.444 +    ((#1 o dest_Const) oo Proof_Context.read_const {proper = true, strict = false});
   2.445 +
   2.446 +val _ =
   2.447 +  hide_names @{command_keyword hide_fact} "facts" Global_Theory.hide_fact
   2.448 +    (Parse.position Parse.xname) (Global_Theory.check_fact o Proof_Context.theory_of);
   2.449 +
   2.450 +in end\<close>
   2.451 +
   2.452 +
   2.453 +subsection \<open>Bundled declarations\<close>
   2.454 +
   2.455 +ML \<open>
   2.456 +local
   2.457  
   2.458  val _ =
   2.459    Outer_Syntax.local_theory @{command_keyword bundle} "define bundle of declarations"
   2.460 @@ -478,8 +498,15 @@
   2.461      "print bundles of declarations"
   2.462      (Parse.opt_bang >> (fn b => Toplevel.keep (Bundle.print_bundles b o Toplevel.context_of)));
   2.463  
   2.464 +in end\<close>
   2.465  
   2.466 -(* local theories *)
   2.467 +
   2.468 +subsection \<open>Local theory specifications\<close>
   2.469 +
   2.470 +subsubsection \<open>Specification context\<close>
   2.471 +
   2.472 +ML \<open>
   2.473 +local
   2.474  
   2.475  val _ =
   2.476    Outer_Syntax.command @{command_keyword context} "begin local theory context"
   2.477 @@ -489,8 +516,19 @@
   2.478          >> (fn (incls, elems) => Toplevel.open_target (#2 o Bundle.context_cmd incls elems)))
   2.479        --| Parse.begin);
   2.480  
   2.481 +val _ =
   2.482 +  Outer_Syntax.command @{command_keyword end} "end context"
   2.483 +    (Scan.succeed
   2.484 +      (Toplevel.exit o Toplevel.end_local_theory o Toplevel.close_target o
   2.485 +        Toplevel.end_proof (K Proof.end_notepad)));
   2.486  
   2.487 -(* locales *)
   2.488 +in end\<close>
   2.489 +
   2.490 +
   2.491 +subsubsection \<open>Locales and interpretation\<close>
   2.492 +
   2.493 +ML \<open>
   2.494 +local
   2.495  
   2.496  val locale_val =
   2.497    Parse_Spec.locale_expression --
   2.498 @@ -532,8 +570,8 @@
   2.499  val _ =
   2.500    Outer_Syntax.local_theory_to_proof @{command_keyword global_interpretation}
   2.501      "prove interpretation of locale expression into global theory"
   2.502 -    (interpretation_args_with_defs
   2.503 -      >> (fn (expr, (defs, equations)) => Interpretation.global_interpretation_cmd expr defs equations));
   2.504 +    (interpretation_args_with_defs >> (fn (expr, (defs, equations)) =>
   2.505 +      Interpretation.global_interpretation_cmd expr defs equations));
   2.506  
   2.507  val _ =
   2.508    Outer_Syntax.command @{command_keyword sublocale}
   2.509 @@ -548,11 +586,16 @@
   2.510    Outer_Syntax.command @{command_keyword interpretation}
   2.511      "prove interpretation of locale expression in local theory or into global theory"
   2.512      (interpretation_args >> (fn (expr, equations) =>
   2.513 -      Toplevel.local_theory_to_proof NONE NONE (Interpretation.isar_interpretation_cmd expr equations)));
   2.514 +      Toplevel.local_theory_to_proof NONE NONE
   2.515 +        (Interpretation.isar_interpretation_cmd expr equations)));
   2.516 +
   2.517 +in end\<close>
   2.518  
   2.519  
   2.520 +subsubsection \<open>Type classes\<close>
   2.521  
   2.522 -(* classes *)
   2.523 +ML \<open>
   2.524 +local
   2.525  
   2.526  val class_val =
   2.527    Parse_Spec.class_expression --
   2.528 @@ -582,8 +625,13 @@
   2.529      Parse.multi_arity >> Class.instance_arity_cmd) >> Toplevel.theory_to_proof ||
   2.530      Scan.succeed (Toplevel.local_theory_to_proof NONE NONE (Class.instantiation_instance I)));
   2.531  
   2.532 +in end\<close>
   2.533  
   2.534 -(* arbitrary overloading *)
   2.535 +
   2.536 +subsubsection \<open>Arbitrary overloading\<close>
   2.537 +
   2.538 +ML \<open>
   2.539 +local
   2.540  
   2.541  val _ =
   2.542    Outer_Syntax.command @{command_keyword overloading} "overloaded definitions"
   2.543 @@ -592,34 +640,30 @@
   2.544        >> Scan.triple1) --| Parse.begin
   2.545     >> (fn operations => Toplevel.begin_local_theory true (Overloading.overloading_cmd operations)));
   2.546  
   2.547 -
   2.548 -(* code generation *)
   2.549 -
   2.550 -val _ =
   2.551 -  Outer_Syntax.command @{command_keyword code_datatype}
   2.552 -    "define set of code datatype constructors"
   2.553 -    (Scan.repeat1 Parse.term >> (Toplevel.theory o Code.add_datatype_cmd));
   2.554 +in end\<close>
   2.555  
   2.556  
   2.557 +subsection \<open>Proof commands\<close>
   2.558  
   2.559 -(** proof commands **)
   2.560 +ML \<open>
   2.561 +local
   2.562  
   2.563  val _ =
   2.564    Outer_Syntax.local_theory_to_proof @{command_keyword notepad} "begin proof context"
   2.565      (Parse.begin >> K Proof.begin_notepad);
   2.566  
   2.567 +in end\<close>
   2.568  
   2.569 -(* statements *)
   2.570 +
   2.571 +subsubsection \<open>Statements\<close>
   2.572 +
   2.573 +ML \<open>
   2.574 +local
   2.575  
   2.576  val structured_statement =
   2.577    Parse_Spec.statement -- Parse_Spec.cond_statement -- Parse.for_fixes
   2.578      >> (fn ((shows, (strict, assumes)), fixes) => (strict, fixes, assumes, shows));
   2.579  
   2.580 -val structured_statement' =
   2.581 -  Parse_Spec.statement -- Parse_Spec.if_statement' -- Parse.for_fixes
   2.582 -    >> (fn ((shows, assumes), fixes) => (fixes, assumes, shows));
   2.583 -
   2.584 -
   2.585  fun theorem spec schematic descr =
   2.586    Outer_Syntax.local_theory_to_proof' spec
   2.587      ("state " ^ descr)
   2.588 @@ -658,8 +702,13 @@
   2.589      (structured_statement >> (fn (a, b, c, d) =>
   2.590        Toplevel.proof' (fn int => Proof.chain #> Proof.show_cmd a NONE (K I) b c d int #> #2)));
   2.591  
   2.592 +in end\<close>
   2.593  
   2.594 -(* facts *)
   2.595 +
   2.596 +subsubsection \<open>Local facts\<close>
   2.597 +
   2.598 +ML \<open>
   2.599 +local
   2.600  
   2.601  val facts = Parse.and_list1 Parse.xthms1;
   2.602  
   2.603 @@ -691,8 +740,17 @@
   2.604    Outer_Syntax.command @{command_keyword unfolding} "unfold definitions in goal and facts"
   2.605      (facts >> (Toplevel.proof o Proof.unfolding_cmd));
   2.606  
   2.607 +in end\<close>
   2.608  
   2.609 -(* proof context *)
   2.610 +
   2.611 +subsubsection \<open>Proof context\<close>
   2.612 +
   2.613 +ML \<open>
   2.614 +local
   2.615 +
   2.616 +val structured_statement =
   2.617 +  Parse_Spec.statement -- Parse_Spec.if_statement' -- Parse.for_fixes
   2.618 +    >> (fn ((shows, assumes), fixes) => (fixes, assumes, shows));
   2.619  
   2.620  val _ =
   2.621    Outer_Syntax.command @{command_keyword fix} "fix local variables (Skolem constants)"
   2.622 @@ -700,11 +758,11 @@
   2.623  
   2.624  val _ =
   2.625    Outer_Syntax.command @{command_keyword assume} "assume propositions"
   2.626 -    (structured_statement' >> (fn (a, b, c) => Toplevel.proof (Proof.assume_cmd a b c)));
   2.627 +    (structured_statement >> (fn (a, b, c) => Toplevel.proof (Proof.assume_cmd a b c)));
   2.628  
   2.629  val _ =
   2.630    Outer_Syntax.command @{command_keyword presume} "assume propositions, to be established later"
   2.631 -    (structured_statement' >> (fn (a, b, c) => Toplevel.proof (Proof.presume_cmd a b c)));
   2.632 +    (structured_statement >> (fn (a, b, c) => Toplevel.proof (Proof.presume_cmd a b c)));
   2.633  
   2.634  val _ =
   2.635    Outer_Syntax.command @{command_keyword def} "local definition (non-polymorphic)"
   2.636 @@ -734,7 +792,7 @@
   2.637  
   2.638  val _ =
   2.639    Outer_Syntax.command @{command_keyword write} "add concrete syntax for constants / fixed variables"
   2.640 -    (opt_mode -- Parse.and_list1 (Parse.const -- Parse.mixfix)
   2.641 +    (Parse.syntax_mode -- Parse.and_list1 (Parse.const -- Parse.mixfix)
   2.642      >> (fn (mode, args) => Toplevel.proof (Proof.write_cmd mode args)));
   2.643  
   2.644  val _ =
   2.645 @@ -745,8 +803,13 @@
   2.646            --| @{keyword ")"}) ||
   2.647          Parse.position Parse.xname >> rpair []) >> (Toplevel.proof o Proof.case_cmd));
   2.648  
   2.649 +in end\<close>
   2.650  
   2.651 -(* proof structure *)
   2.652 +
   2.653 +subsubsection \<open>Proof structure\<close>
   2.654 +
   2.655 +ML \<open>
   2.656 +local
   2.657  
   2.658  val _ =
   2.659    Outer_Syntax.command @{command_keyword "{"} "begin explicit proof block"
   2.660 @@ -760,8 +823,13 @@
   2.661    Outer_Syntax.command @{command_keyword next} "enter next proof block"
   2.662      (Scan.succeed (Toplevel.proof Proof.next_block));
   2.663  
   2.664 +in end\<close>
   2.665  
   2.666 -(* end proof *)
   2.667 +
   2.668 +subsubsection \<open>End proof\<close>
   2.669 +
   2.670 +ML \<open>
   2.671 +local
   2.672  
   2.673  val _ =
   2.674    Outer_Syntax.command @{command_keyword qed} "conclude proof"
   2.675 @@ -800,8 +868,13 @@
   2.676    Outer_Syntax.command @{command_keyword oops} "forget proof"
   2.677      (Scan.succeed (Toplevel.forget_proof true));
   2.678  
   2.679 +in end\<close>
   2.680  
   2.681 -(* proof steps *)
   2.682 +
   2.683 +subsubsection \<open>Proof steps\<close>
   2.684 +
   2.685 +ML \<open>
   2.686 +local
   2.687  
   2.688  val _ =
   2.689    Outer_Syntax.command @{command_keyword defer} "shuffle internal proof state"
   2.690 @@ -824,9 +897,12 @@
   2.691      (Scan.option Method.parse >> (fn m =>
   2.692        (Option.map Method.report m; Toplevel.proofs (Proof.proof m))));
   2.693  
   2.694 +in end\<close>
   2.695  
   2.696 -(* subgoal focus *)
   2.697  
   2.698 +subsubsection \<open>Subgoal focus\<close>
   2.699 +
   2.700 +ML \<open>
   2.701  local
   2.702  
   2.703  val opt_fact_binding =
   2.704 @@ -840,8 +916,6 @@
   2.705          (Scan.repeat1 (Parse.position (Parse.maybe Parse.name)))))
   2.706      (false, []);
   2.707  
   2.708 -in
   2.709 -
   2.710  val _ =
   2.711    Outer_Syntax.command @{command_keyword subgoal}
   2.712      "focus on first subgoal within backward refinement"
   2.713 @@ -849,10 +923,13 @@
   2.714        for_params >> (fn ((a, b), c) =>
   2.715          Toplevel.proofs (Seq.make_results o Seq.single o #2 o Subgoal.subgoal_cmd a b c)));
   2.716  
   2.717 -end;
   2.718 +in end\<close>
   2.719  
   2.720  
   2.721 -(* calculation *)
   2.722 +subsubsection \<open>Calculation\<close>
   2.723 +
   2.724 +ML \<open>
   2.725 +local
   2.726  
   2.727  val calculation_args =
   2.728    Scan.option (@{keyword "("} |-- Parse.!!! ((Parse.xthms1 --| @{keyword ")"})));
   2.729 @@ -879,8 +956,13 @@
   2.730    Outer_Syntax.command @{command_keyword print_trans_rules} "print transitivity rules"
   2.731      (Scan.succeed (Toplevel.keep (Calculation.print_rules o Toplevel.context_of)));
   2.732  
   2.733 +in end\<close>
   2.734  
   2.735 -(* proof navigation *)
   2.736 +
   2.737 +subsubsection \<open>Proof navigation\<close>
   2.738 +
   2.739 +ML \<open>
   2.740 +local
   2.741  
   2.742  fun report_back () =
   2.743    Output.report [Markup.markup Markup.bad "Explicit backtracking"];
   2.744 @@ -891,9 +973,13 @@
   2.745       (Toplevel.actual_proof (fn prf => (report_back (); Proof_Node.back prf)) o
   2.746        Toplevel.skip_proof report_back));
   2.747  
   2.748 +in end\<close>
   2.749  
   2.750  
   2.751 -(** diagnostic commands (for interactive mode only) **)
   2.752 +subsection \<open>Diagnostic commands (for interactive mode only)\<close>
   2.753 +
   2.754 +ML \<open>
   2.755 +local
   2.756  
   2.757  val opt_modes =
   2.758    Scan.optional (@{keyword "("} |-- Parse.!!! (Scan.repeat1 Parse.xname --| @{keyword ")"})) [];
   2.759 @@ -1087,34 +1173,33 @@
   2.760      (Scan.repeat1 Parse.path >> (fn names =>
   2.761        Toplevel.keep (fn _ => ignore (Present.display_drafts (map Path.explode names)))));
   2.762  
   2.763 +in end\<close>
   2.764  
   2.765 -(* deps *)
   2.766  
   2.767 +subsection \<open>Dependencies\<close>
   2.768 +
   2.769 +ML \<open>
   2.770  local
   2.771 -  val theory_bounds =
   2.772 -    Parse.position Parse.theory_xname >> single ||
   2.773 -    (@{keyword "("} |-- Parse.enum "|" (Parse.position Parse.theory_xname) --| @{keyword ")"});
   2.774 -in
   2.775 +
   2.776 +val theory_bounds =
   2.777 +  Parse.position Parse.theory_xname >> single ||
   2.778 +  (@{keyword "("} |-- Parse.enum "|" (Parse.position Parse.theory_xname) --| @{keyword ")"});
   2.779  
   2.780  val _ =
   2.781    Outer_Syntax.command @{command_keyword thy_deps} "visualize theory dependencies"
   2.782      (Scan.option theory_bounds -- Scan.option theory_bounds >>
   2.783        (fn args => Toplevel.keep (fn st => Thy_Deps.thy_deps_cmd (Toplevel.context_of st) args)));
   2.784  
   2.785 -end;
   2.786  
   2.787 -local
   2.788 -  val class_bounds =
   2.789 -    Parse.sort >> single ||
   2.790 -    (@{keyword "("} |-- Parse.enum "|" Parse.sort --| @{keyword ")"});
   2.791 -in
   2.792 +val class_bounds =
   2.793 +  Parse.sort >> single ||
   2.794 +  (@{keyword "("} |-- Parse.enum "|" Parse.sort --| @{keyword ")"});
   2.795  
   2.796  val _ =
   2.797    Outer_Syntax.command @{command_keyword class_deps} "visualize class dependencies"
   2.798      (Scan.option class_bounds -- Scan.option class_bounds >> (fn args =>
   2.799        Toplevel.keep (fn st => Class_Deps.class_deps_cmd (Toplevel.context_of st) args)));
   2.800  
   2.801 -end;
   2.802  
   2.803  val _ =
   2.804    Outer_Syntax.command @{command_keyword thm_deps} "visualize theorem dependencies"
   2.805 @@ -1123,10 +1208,9 @@
   2.806          Thm_Deps.thm_deps (Toplevel.theory_of st)
   2.807            (Attrib.eval_thms (Toplevel.context_of st) args))));
   2.808  
   2.809 -local
   2.810 -  val thy_names =
   2.811 -    Scan.repeat1 (Scan.unless Parse.minus (Parse.position Parse.theory_xname));
   2.812 -in
   2.813 +
   2.814 +val thy_names =
   2.815 +  Scan.repeat1 (Scan.unless Parse.minus (Parse.position Parse.theory_xname));
   2.816  
   2.817  val _ =
   2.818    Outer_Syntax.command @{command_keyword unused_thms} "find unused theorems"
   2.819 @@ -1146,10 +1230,13 @@
   2.820              |> map pretty_thm |> Pretty.writeln_chunks
   2.821            end)));
   2.822  
   2.823 -end;
   2.824 +in end\<close>
   2.825  
   2.826  
   2.827 -(* find *)
   2.828 +subsubsection \<open>Find consts and theorems\<close>
   2.829 +
   2.830 +ML \<open>
   2.831 +local
   2.832  
   2.833  val _ =
   2.834    Outer_Syntax.command @{command_keyword find_consts}
   2.835 @@ -1158,14 +1245,12 @@
   2.836        Toplevel.keep (fn st =>
   2.837          Pretty.writeln (Find_Consts.pretty_consts (Toplevel.context_of st) spec))));
   2.838  
   2.839 -local
   2.840 -  val options =
   2.841 -    Scan.optional
   2.842 -      (Parse.$$$ "(" |--
   2.843 -        Parse.!!! (Scan.option Parse.nat --
   2.844 -          Scan.optional (Parse.reserved "with_dups" >> K false) true --| Parse.$$$ ")"))
   2.845 -      (NONE, true);
   2.846 -in
   2.847 +val options =
   2.848 +  Scan.optional
   2.849 +    (Parse.$$$ "(" |--
   2.850 +      Parse.!!! (Scan.option Parse.nat --
   2.851 +        Scan.optional (Parse.reserved "with_dups" >> K false) true --| Parse.$$$ ")"))
   2.852 +    (NONE, true);
   2.853  
   2.854  val _ =
   2.855    Outer_Syntax.command @{command_keyword find_theorems}
   2.856 @@ -1175,11 +1260,26 @@
   2.857          Pretty.writeln
   2.858            (Find_Theorems.pretty_theorems (Find_Theorems.proof_state st) opt_lim rem_dups spec))));
   2.859  
   2.860 -end;
   2.861 +in end\<close>
   2.862  
   2.863  
   2.864 +subsection \<open>Code generation\<close>
   2.865  
   2.866 -(** extraction of programs from proofs **)
   2.867 +ML \<open>
   2.868 +local
   2.869 +
   2.870 +val _ =
   2.871 +  Outer_Syntax.command @{command_keyword code_datatype}
   2.872 +    "define set of code datatype constructors"
   2.873 +    (Scan.repeat1 Parse.term >> (Toplevel.theory o Code.add_datatype_cmd));
   2.874 +
   2.875 +in end\<close>
   2.876 +
   2.877 +
   2.878 +subsection \<open>Extraction of programs from proofs\<close>
   2.879 +
   2.880 +ML \<open>
   2.881 +local
   2.882  
   2.883  val parse_vars = Scan.optional (Parse.$$$ "(" |-- Parse.list1 Parse.name --| Parse.$$$ ")") [];
   2.884  
   2.885 @@ -1205,21 +1305,10 @@
   2.886      (Scan.repeat1 (Parse.xname -- parse_vars) >> (fn xs => Toplevel.theory (fn thy =>
   2.887        Extraction.extract (map (apfst (Global_Theory.get_thm thy)) xs) thy)));
   2.888  
   2.889 +in end\<close>
   2.890  
   2.891  
   2.892 -(** end **)
   2.893 -
   2.894 -val _ =
   2.895 -  Outer_Syntax.command @{command_keyword end} "end context"
   2.896 -    (Scan.succeed
   2.897 -      (Toplevel.exit o Toplevel.end_local_theory o Toplevel.close_target o
   2.898 -        Toplevel.end_proof (K Proof.end_notepad)));
   2.899 -
   2.900 -in end;
   2.901 -\<close>
   2.902 -
   2.903 -
   2.904 -section \<open>Basic attributes\<close>
   2.905 +section \<open>Isar attributes\<close>
   2.906  
   2.907  attribute_setup tagged =
   2.908    \<open>Scan.lift (Args.name -- Args.name) >> Thm.tag\<close>