# HG changeset patch
# User wenzelm
# Date 1459800788 -7200
# Node ID 3f97aa4580c67760c41ec02fe0f069f37738f54b
# Parent  82859dac5f59d785aecb4bcd8a8b44749ced3a72
tuned -- more explicit sections;

diff -r 82859dac5f59 -r 3f97aa4580c6 src/Pure/Isar/parse.ML
--- a/src/Pure/Isar/parse.ML	Mon Apr 04 20:46:39 2016 +0200
+++ b/src/Pure/Isar/parse.ML	Mon Apr 04 22:13:08 2016 +0200
@@ -85,6 +85,7 @@
   val mixfix': mixfix parser
   val opt_mixfix: mixfix parser
   val opt_mixfix': mixfix parser
+  val syntax_mode: Syntax.mode parser
   val where_: string parser
   val const_decl: (string * string * mixfix) parser
   val const_binding: (binding * string * mixfix) parser
@@ -356,6 +357,15 @@
 end;
 
 
+(* syntax mode *)
+
+val syntax_mode_spec =
+  ($$$ "output" >> K ("", false)) || name -- Scan.optional ($$$ "output" >> K false) true;
+
+val syntax_mode =
+  Scan.optional ($$$ "(" |-- !!! (syntax_mode_spec --| $$$ ")")) Syntax.mode_default;
+
+
 (* fixes *)
 
 val where_ = $$$ "where";
diff -r 82859dac5f59 -r 3f97aa4580c6 src/Pure/Pure.thy
--- a/src/Pure/Pure.thy	Mon Apr 04 20:46:39 2016 +0200
+++ b/src/Pure/Pure.thy	Mon Apr 04 22:13:08 2016 +0200
@@ -95,191 +95,9 @@
 
 section \<open>Isar commands\<close>
 
-ML \<open>
-local
-
-(** theory commands **)
-
-(* sorts *)
-
-val _ =
-  Outer_Syntax.local_theory @{command_keyword default_sort}
-    "declare default sort for explicit type variables"
-    (Parse.sort >> (fn s => fn lthy => Local_Theory.set_defsort (Syntax.read_sort lthy s) lthy));
-
-
-(* types *)
-
-val _ =
-  Outer_Syntax.local_theory @{command_keyword typedecl} "type declaration"
-    (Parse.type_args -- Parse.binding -- Parse.opt_mixfix
-      >> (fn ((args, a), mx) =>
-          Typedecl.typedecl {final = true} (a, map (rpair dummyS) args, mx) #> snd));
-
-val _ =
-  Outer_Syntax.local_theory @{command_keyword type_synonym} "declare type abbreviation"
-    (Parse.type_args -- Parse.binding --
-      (@{keyword "="} |-- Parse.!!! (Parse.typ -- Parse.opt_mixfix'))
-      >> (fn ((args, a), (rhs, mx)) => snd o Typedecl.abbrev_cmd (a, args, mx) rhs));
-
-val _ =
-  Outer_Syntax.command @{command_keyword nonterminal}
-    "declare syntactic type constructors (grammar nonterminal symbols)"
-    (Parse.and_list1 Parse.binding >> (Toplevel.theory o Sign.add_nonterminals_global));
-
-
-(* consts and syntax *)
-
-val _ =
-  Outer_Syntax.command @{command_keyword judgment} "declare object-logic judgment"
-    (Parse.const_binding >> (Toplevel.theory o Object_Logic.add_judgment_cmd));
-
-val _ =
-  Outer_Syntax.command @{command_keyword consts} "declare constants"
-    (Scan.repeat1 Parse.const_binding >> (Toplevel.theory o Sign.add_consts_cmd));
-
-val mode_spec =
-  (@{keyword "output"} >> K ("", false)) ||
-    Parse.name -- Scan.optional (@{keyword "output"} >> K false) true;
-
-val opt_mode =
-  Scan.optional (@{keyword "("} |-- Parse.!!! (mode_spec --| @{keyword ")"})) Syntax.mode_default;
-
-val _ =
-  Outer_Syntax.command @{command_keyword syntax} "add raw syntax clauses"
-    (opt_mode -- Scan.repeat1 Parse.const_decl
-      >> (Toplevel.theory o uncurry Sign.add_syntax_cmd));
-
-val _ =
-  Outer_Syntax.command @{command_keyword no_syntax} "delete raw syntax clauses"
-    (opt_mode -- Scan.repeat1 Parse.const_decl
-      >> (Toplevel.theory o uncurry Sign.del_syntax_cmd));
-
-
-(* translations *)
-
-val trans_pat =
-  Scan.optional
-    (@{keyword "("} |-- Parse.!!! (Parse.inner_syntax Parse.xname --| @{keyword ")"})) "logic"
-    -- Parse.inner_syntax Parse.string;
-
-fun trans_arrow toks =
-  ((@{keyword "\<rightharpoonup>"} || @{keyword "=>"}) >> K Syntax.Parse_Rule ||
-    (@{keyword "\<leftharpoondown>"} || @{keyword "<="}) >> K Syntax.Print_Rule ||
-    (@{keyword "\<rightleftharpoons>"} || @{keyword "=="}) >> K Syntax.Parse_Print_Rule) toks;
-
-val trans_line =
-  trans_pat -- Parse.!!! (trans_arrow -- trans_pat)
-    >> (fn (left, (arr, right)) => arr (left, right));
-
-val _ =
-  Outer_Syntax.command @{command_keyword translations} "add syntax translation rules"
-    (Scan.repeat1 trans_line >> (Toplevel.theory o Isar_Cmd.translations));
-
-val _ =
-  Outer_Syntax.command @{command_keyword no_translations} "delete syntax translation rules"
-    (Scan.repeat1 trans_line >> (Toplevel.theory o Isar_Cmd.no_translations));
-
-
-(* constant definitions and abbreviations *)
-
-val _ =
-  Outer_Syntax.local_theory' @{command_keyword definition} "constant definition"
-    (Parse_Spec.constdef >> (fn args => #2 oo Specification.definition_cmd args));
+subsection \<open>Embedded ML text\<close>
 
-val _ =
-  Outer_Syntax.local_theory' @{command_keyword abbreviation} "constant abbreviation"
-    (opt_mode -- (Scan.option Parse_Spec.constdecl -- Parse.prop)
-      >> (fn (mode, args) => Specification.abbreviation_cmd mode args));
-
-val _ =
-  Outer_Syntax.local_theory @{command_keyword type_notation}
-    "add concrete syntax for type constructors"
-    (opt_mode -- Parse.and_list1 (Parse.type_const -- Parse.mixfix)
-      >> (fn (mode, args) => Specification.type_notation_cmd true mode args));
-
-val _ =
-  Outer_Syntax.local_theory @{command_keyword no_type_notation}
-    "delete concrete syntax for type constructors"
-    (opt_mode -- Parse.and_list1 (Parse.type_const -- Parse.mixfix)
-      >> (fn (mode, args) => Specification.type_notation_cmd false mode args));
-
-val _ =
-  Outer_Syntax.local_theory @{command_keyword notation}
-    "add concrete syntax for constants / fixed variables"
-    (opt_mode -- Parse.and_list1 (Parse.const -- Parse.mixfix)
-      >> (fn (mode, args) => Specification.notation_cmd true mode args));
-
-val _ =
-  Outer_Syntax.local_theory @{command_keyword no_notation}
-    "delete concrete syntax for constants / fixed variables"
-    (opt_mode -- Parse.and_list1 (Parse.const -- Parse.mixfix)
-      >> (fn (mode, args) => Specification.notation_cmd false mode args));
-
-
-(* constant specifications *)
-
-val _ =
-  Outer_Syntax.command @{command_keyword axiomatization} "axiomatic constant specification"
-    (Scan.optional Parse.fixes [] --
-      Scan.optional (Parse.where_ |-- Parse.!!! (Parse.and_list1 Parse_Spec.specs)) []
-      >> (fn (x, y) => Toplevel.theory (#2 o Specification.axiomatization_cmd x y)));
-
-
-(* theorems *)
-
-val _ =
-  Outer_Syntax.local_theory' @{command_keyword lemmas} "define theorems"
-    (Parse_Spec.name_facts -- Parse.for_fixes >>
-      (fn (facts, fixes) => #2 oo Specification.theorems_cmd Thm.theoremK facts fixes));
-
-val _ =
-  Outer_Syntax.local_theory' @{command_keyword declare} "declare theorems"
-    (Parse.and_list1 Parse.xthms1 -- Parse.for_fixes
-      >> (fn (facts, fixes) =>
-          #2 oo Specification.theorems_cmd "" [(Attrib.empty_binding, flat facts)] fixes));
-
-val _ =
-  Outer_Syntax.local_theory @{command_keyword named_theorems}
-    "declare named collection of theorems"
-    (Parse.and_list1 (Parse.binding -- Scan.optional Parse.text "") >>
-      fold (fn (b, descr) => snd o Named_Theorems.declare b descr));
-
-
-(* hide names *)
-
-local
-
-fun hide_names command_keyword what hide parse prep =
-  Outer_Syntax.command command_keyword ("hide " ^ what ^ " from name space")
-    ((Parse.opt_keyword "open" >> not) -- Scan.repeat1 parse >> (fn (fully, args) =>
-      (Toplevel.theory (fn thy =>
-        let val ctxt = Proof_Context.init_global thy
-        in fold (hide fully o prep ctxt) args thy end))));
-
-in
-
-val _ =
-  hide_names @{command_keyword hide_class} "classes" Sign.hide_class Parse.class
-    Proof_Context.read_class;
-
-val _ =
-  hide_names @{command_keyword hide_type} "types" Sign.hide_type Parse.type_const
-    ((#1 o dest_Type) oo Proof_Context.read_type_name {proper = true, strict = false});
-
-val _ =
-  hide_names @{command_keyword hide_const} "consts" Sign.hide_const Parse.const
-    ((#1 o dest_Const) oo Proof_Context.read_const {proper = true, strict = false});
-
-val _ =
-  hide_names @{command_keyword hide_fact} "facts" Global_Theory.hide_fact
-    (Parse.position Parse.xname) (Global_Theory.check_fact o Proof_Context.theory_of);
-
-end;
-
-
-(* use ML text *)
-
+ML \<open>
 local
 
 fun ML_file_cmd debug files = Toplevel.generic_theory (fn gthy =>
@@ -309,8 +127,6 @@
       (ML_Context.exec (fn () => ML_Context.eval_source flags source))
   end);
 
-in
-
 val _ =
   Outer_Syntax.command ("ML_file", @{here}) "read and evaluate Isabelle/ML file"
     (Resources.parse_files "ML_file" >> ML_file_cmd NONE);
@@ -339,8 +155,6 @@
     "read and evaluate Standard ML file (no debugger information)"
     (Resources.provide_parse_files "SML_file_no_debug" >> SML_file_cmd (SOME false));
 
-end;
-
 val _ =
   Outer_Syntax.command @{command_keyword SML_export} "evaluate SML within Isabelle/ML environment"
     (Parse.ML_source >> (fn source =>
@@ -391,6 +205,11 @@
     (Parse.ML_source >> Isar_Cmd.local_setup);
 
 val _ =
+  Outer_Syntax.command @{command_keyword oracle} "declare oracle"
+    (Parse.range Parse.name -- (@{keyword "="} |-- Parse.ML_source) >>
+      (fn (x, y) => Toplevel.theory (Isar_Cmd.oracle x y)));
+
+val _ =
   Outer_Syntax.local_theory @{command_keyword attribute_setup} "define attribute in ML"
     (Parse.position Parse.name --
         Parse.!!! (@{keyword "="} |-- Parse.ML_source -- Scan.optional Parse.text "")
@@ -419,8 +238,101 @@
       Parse.ML_source -- Scan.optional (@{keyword "identifier"} |-- Scan.repeat1 Parse.xname) []
     >> (fn (((a, b), c), d) => Isar_Cmd.simproc_setup a b c d));
 
+in end\<close>
 
-(* translation functions *)
+
+subsection \<open>Theory commands\<close>
+
+subsubsection \<open>Sorts and types\<close>
+
+ML \<open>
+local
+
+val _ =
+  Outer_Syntax.local_theory @{command_keyword default_sort}
+    "declare default sort for explicit type variables"
+    (Parse.sort >> (fn s => fn lthy => Local_Theory.set_defsort (Syntax.read_sort lthy s) lthy));
+
+val _ =
+  Outer_Syntax.local_theory @{command_keyword typedecl} "type declaration"
+    (Parse.type_args -- Parse.binding -- Parse.opt_mixfix
+      >> (fn ((args, a), mx) =>
+          Typedecl.typedecl {final = true} (a, map (rpair dummyS) args, mx) #> snd));
+
+val _ =
+  Outer_Syntax.local_theory @{command_keyword type_synonym} "declare type abbreviation"
+    (Parse.type_args -- Parse.binding --
+      (@{keyword "="} |-- Parse.!!! (Parse.typ -- Parse.opt_mixfix'))
+      >> (fn ((args, a), (rhs, mx)) => snd o Typedecl.abbrev_cmd (a, args, mx) rhs));
+
+in end\<close>
+
+
+subsubsection \<open>Consts\<close>
+
+ML \<open>
+local
+
+val _ =
+  Outer_Syntax.command @{command_keyword judgment} "declare object-logic judgment"
+    (Parse.const_binding >> (Toplevel.theory o Object_Logic.add_judgment_cmd));
+
+val _ =
+  Outer_Syntax.command @{command_keyword consts} "declare constants"
+    (Scan.repeat1 Parse.const_binding >> (Toplevel.theory o Sign.add_consts_cmd));
+
+in end\<close>
+
+
+subsubsection \<open>Syntax and translations\<close>
+
+ML \<open>
+local
+
+val _ =
+  Outer_Syntax.command @{command_keyword nonterminal}
+    "declare syntactic type constructors (grammar nonterminal symbols)"
+    (Parse.and_list1 Parse.binding >> (Toplevel.theory o Sign.add_nonterminals_global));
+
+val _ =
+  Outer_Syntax.command @{command_keyword syntax} "add raw syntax clauses"
+    (Parse.syntax_mode -- Scan.repeat1 Parse.const_decl
+      >> (Toplevel.theory o uncurry Sign.add_syntax_cmd));
+
+val _ =
+  Outer_Syntax.command @{command_keyword no_syntax} "delete raw syntax clauses"
+    (Parse.syntax_mode -- Scan.repeat1 Parse.const_decl
+      >> (Toplevel.theory o uncurry Sign.del_syntax_cmd));
+
+val trans_pat =
+  Scan.optional
+    (@{keyword "("} |-- Parse.!!! (Parse.inner_syntax Parse.xname --| @{keyword ")"})) "logic"
+    -- Parse.inner_syntax Parse.string;
+
+fun trans_arrow toks =
+  ((@{keyword "\<rightharpoonup>"} || @{keyword "=>"}) >> K Syntax.Parse_Rule ||
+    (@{keyword "\<leftharpoondown>"} || @{keyword "<="}) >> K Syntax.Print_Rule ||
+    (@{keyword "\<rightleftharpoons>"} || @{keyword "=="}) >> K Syntax.Parse_Print_Rule) toks;
+
+val trans_line =
+  trans_pat -- Parse.!!! (trans_arrow -- trans_pat)
+    >> (fn (left, (arr, right)) => arr (left, right));
+
+val _ =
+  Outer_Syntax.command @{command_keyword translations} "add syntax translation rules"
+    (Scan.repeat1 trans_line >> (Toplevel.theory o Isar_Cmd.translations));
+
+val _ =
+  Outer_Syntax.command @{command_keyword no_translations} "delete syntax translation rules"
+    (Scan.repeat1 trans_line >> (Toplevel.theory o Isar_Cmd.no_translations));
+
+in end\<close>
+
+
+subsubsection \<open>Translation functions\<close>
+
+ML \<open>
+local
 
 val _ =
   Outer_Syntax.command @{command_keyword parse_ast_translation}
@@ -447,16 +359,124 @@
     "install print ast translation functions"
     (Parse.ML_source >> (Toplevel.theory o Isar_Cmd.print_ast_translation));
 
+in end\<close>
 
-(* oracles *)
+
+subsubsection \<open>Specifications\<close>
+
+ML \<open>
+local
+
+val _ =
+  Outer_Syntax.local_theory' @{command_keyword definition} "constant definition"
+    (Parse_Spec.constdef >> (fn args => #2 oo Specification.definition_cmd args));
+
+val _ =
+  Outer_Syntax.local_theory' @{command_keyword abbreviation} "constant abbreviation"
+    (Parse.syntax_mode -- (Scan.option Parse_Spec.constdecl -- Parse.prop)
+      >> (fn (mode, args) => Specification.abbreviation_cmd mode args));
+
+val _ =
+  Outer_Syntax.command @{command_keyword axiomatization} "axiomatic constant specification"
+    (Scan.optional Parse.fixes [] --
+      Scan.optional (Parse.where_ |-- Parse.!!! (Parse.and_list1 Parse_Spec.specs)) []
+      >> (fn (x, y) => Toplevel.theory (#2 o Specification.axiomatization_cmd x y)));
+
+in end\<close>
+
+
+subsubsection \<open>Notation\<close>
+
+ML \<open>
+local
+
+val _ =
+  Outer_Syntax.local_theory @{command_keyword type_notation}
+    "add concrete syntax for type constructors"
+    (Parse.syntax_mode -- Parse.and_list1 (Parse.type_const -- Parse.mixfix)
+      >> (fn (mode, args) => Specification.type_notation_cmd true mode args));
+
+val _ =
+  Outer_Syntax.local_theory @{command_keyword no_type_notation}
+    "delete concrete syntax for type constructors"
+    (Parse.syntax_mode -- Parse.and_list1 (Parse.type_const -- Parse.mixfix)
+      >> (fn (mode, args) => Specification.type_notation_cmd false mode args));
+
+val _ =
+  Outer_Syntax.local_theory @{command_keyword notation}
+    "add concrete syntax for constants / fixed variables"
+    (Parse.syntax_mode -- Parse.and_list1 (Parse.const -- Parse.mixfix)
+      >> (fn (mode, args) => Specification.notation_cmd true mode args));
 
 val _ =
-  Outer_Syntax.command @{command_keyword oracle} "declare oracle"
-    (Parse.range Parse.name -- (@{keyword "="} |-- Parse.ML_source) >>
-      (fn (x, y) => Toplevel.theory (Isar_Cmd.oracle x y)));
+  Outer_Syntax.local_theory @{command_keyword no_notation}
+    "delete concrete syntax for constants / fixed variables"
+    (Parse.syntax_mode -- Parse.and_list1 (Parse.const -- Parse.mixfix)
+      >> (fn (mode, args) => Specification.notation_cmd false mode args));
+
+in end\<close>
+
+
+subsubsection \<open>Theorems\<close>
+
+ML \<open>
+local
+
+val _ =
+  Outer_Syntax.local_theory' @{command_keyword lemmas} "define theorems"
+    (Parse_Spec.name_facts -- Parse.for_fixes >>
+      (fn (facts, fixes) => #2 oo Specification.theorems_cmd Thm.theoremK facts fixes));
+
+val _ =
+  Outer_Syntax.local_theory' @{command_keyword declare} "declare theorems"
+    (Parse.and_list1 Parse.xthms1 -- Parse.for_fixes
+      >> (fn (facts, fixes) =>
+          #2 oo Specification.theorems_cmd "" [(Attrib.empty_binding, flat facts)] fixes));
+
+val _ =
+  Outer_Syntax.local_theory @{command_keyword named_theorems}
+    "declare named collection of theorems"
+    (Parse.and_list1 (Parse.binding -- Scan.optional Parse.text "") >>
+      fold (fn (b, descr) => snd o Named_Theorems.declare b descr));
+
+in end\<close>
 
 
-(* bundled declarations *)
+subsubsection \<open>Hide names\<close>
+
+ML \<open>
+local
+
+fun hide_names command_keyword what hide parse prep =
+  Outer_Syntax.command command_keyword ("hide " ^ what ^ " from name space")
+    ((Parse.opt_keyword "open" >> not) -- Scan.repeat1 parse >> (fn (fully, args) =>
+      (Toplevel.theory (fn thy =>
+        let val ctxt = Proof_Context.init_global thy
+        in fold (hide fully o prep ctxt) args thy end))));
+
+val _ =
+  hide_names @{command_keyword hide_class} "classes" Sign.hide_class Parse.class
+    Proof_Context.read_class;
+
+val _ =
+  hide_names @{command_keyword hide_type} "types" Sign.hide_type Parse.type_const
+    ((#1 o dest_Type) oo Proof_Context.read_type_name {proper = true, strict = false});
+
+val _ =
+  hide_names @{command_keyword hide_const} "consts" Sign.hide_const Parse.const
+    ((#1 o dest_Const) oo Proof_Context.read_const {proper = true, strict = false});
+
+val _ =
+  hide_names @{command_keyword hide_fact} "facts" Global_Theory.hide_fact
+    (Parse.position Parse.xname) (Global_Theory.check_fact o Proof_Context.theory_of);
+
+in end\<close>
+
+
+subsection \<open>Bundled declarations\<close>
+
+ML \<open>
+local
 
 val _ =
   Outer_Syntax.local_theory @{command_keyword bundle} "define bundle of declarations"
@@ -478,8 +498,15 @@
     "print bundles of declarations"
     (Parse.opt_bang >> (fn b => Toplevel.keep (Bundle.print_bundles b o Toplevel.context_of)));
 
+in end\<close>
 
-(* local theories *)
+
+subsection \<open>Local theory specifications\<close>
+
+subsubsection \<open>Specification context\<close>
+
+ML \<open>
+local
 
 val _ =
   Outer_Syntax.command @{command_keyword context} "begin local theory context"
@@ -489,8 +516,19 @@
         >> (fn (incls, elems) => Toplevel.open_target (#2 o Bundle.context_cmd incls elems)))
       --| Parse.begin);
 
+val _ =
+  Outer_Syntax.command @{command_keyword end} "end context"
+    (Scan.succeed
+      (Toplevel.exit o Toplevel.end_local_theory o Toplevel.close_target o
+        Toplevel.end_proof (K Proof.end_notepad)));
 
-(* locales *)
+in end\<close>
+
+
+subsubsection \<open>Locales and interpretation\<close>
+
+ML \<open>
+local
 
 val locale_val =
   Parse_Spec.locale_expression --
@@ -532,8 +570,8 @@
 val _ =
   Outer_Syntax.local_theory_to_proof @{command_keyword global_interpretation}
     "prove interpretation of locale expression into global theory"
-    (interpretation_args_with_defs
-      >> (fn (expr, (defs, equations)) => Interpretation.global_interpretation_cmd expr defs equations));
+    (interpretation_args_with_defs >> (fn (expr, (defs, equations)) =>
+      Interpretation.global_interpretation_cmd expr defs equations));
 
 val _ =
   Outer_Syntax.command @{command_keyword sublocale}
@@ -548,11 +586,16 @@
   Outer_Syntax.command @{command_keyword interpretation}
     "prove interpretation of locale expression in local theory or into global theory"
     (interpretation_args >> (fn (expr, equations) =>
-      Toplevel.local_theory_to_proof NONE NONE (Interpretation.isar_interpretation_cmd expr equations)));
+      Toplevel.local_theory_to_proof NONE NONE
+        (Interpretation.isar_interpretation_cmd expr equations)));
+
+in end\<close>
 
 
+subsubsection \<open>Type classes\<close>
 
-(* classes *)
+ML \<open>
+local
 
 val class_val =
   Parse_Spec.class_expression --
@@ -582,8 +625,13 @@
     Parse.multi_arity >> Class.instance_arity_cmd) >> Toplevel.theory_to_proof ||
     Scan.succeed (Toplevel.local_theory_to_proof NONE NONE (Class.instantiation_instance I)));
 
+in end\<close>
 
-(* arbitrary overloading *)
+
+subsubsection \<open>Arbitrary overloading\<close>
+
+ML \<open>
+local
 
 val _ =
   Outer_Syntax.command @{command_keyword overloading} "overloaded definitions"
@@ -592,34 +640,30 @@
       >> Scan.triple1) --| Parse.begin
    >> (fn operations => Toplevel.begin_local_theory true (Overloading.overloading_cmd operations)));
 
-
-(* code generation *)
-
-val _ =
-  Outer_Syntax.command @{command_keyword code_datatype}
-    "define set of code datatype constructors"
-    (Scan.repeat1 Parse.term >> (Toplevel.theory o Code.add_datatype_cmd));
+in end\<close>
 
 
+subsection \<open>Proof commands\<close>
 
-(** proof commands **)
+ML \<open>
+local
 
 val _ =
   Outer_Syntax.local_theory_to_proof @{command_keyword notepad} "begin proof context"
     (Parse.begin >> K Proof.begin_notepad);
 
+in end\<close>
 
-(* statements *)
+
+subsubsection \<open>Statements\<close>
+
+ML \<open>
+local
 
 val structured_statement =
   Parse_Spec.statement -- Parse_Spec.cond_statement -- Parse.for_fixes
     >> (fn ((shows, (strict, assumes)), fixes) => (strict, fixes, assumes, shows));
 
-val structured_statement' =
-  Parse_Spec.statement -- Parse_Spec.if_statement' -- Parse.for_fixes
-    >> (fn ((shows, assumes), fixes) => (fixes, assumes, shows));
-
-
 fun theorem spec schematic descr =
   Outer_Syntax.local_theory_to_proof' spec
     ("state " ^ descr)
@@ -658,8 +702,13 @@
     (structured_statement >> (fn (a, b, c, d) =>
       Toplevel.proof' (fn int => Proof.chain #> Proof.show_cmd a NONE (K I) b c d int #> #2)));
 
+in end\<close>
 
-(* facts *)
+
+subsubsection \<open>Local facts\<close>
+
+ML \<open>
+local
 
 val facts = Parse.and_list1 Parse.xthms1;
 
@@ -691,8 +740,17 @@
   Outer_Syntax.command @{command_keyword unfolding} "unfold definitions in goal and facts"
     (facts >> (Toplevel.proof o Proof.unfolding_cmd));
 
+in end\<close>
 
-(* proof context *)
+
+subsubsection \<open>Proof context\<close>
+
+ML \<open>
+local
+
+val structured_statement =
+  Parse_Spec.statement -- Parse_Spec.if_statement' -- Parse.for_fixes
+    >> (fn ((shows, assumes), fixes) => (fixes, assumes, shows));
 
 val _ =
   Outer_Syntax.command @{command_keyword fix} "fix local variables (Skolem constants)"
@@ -700,11 +758,11 @@
 
 val _ =
   Outer_Syntax.command @{command_keyword assume} "assume propositions"
-    (structured_statement' >> (fn (a, b, c) => Toplevel.proof (Proof.assume_cmd a b c)));
+    (structured_statement >> (fn (a, b, c) => Toplevel.proof (Proof.assume_cmd a b c)));
 
 val _ =
   Outer_Syntax.command @{command_keyword presume} "assume propositions, to be established later"
-    (structured_statement' >> (fn (a, b, c) => Toplevel.proof (Proof.presume_cmd a b c)));
+    (structured_statement >> (fn (a, b, c) => Toplevel.proof (Proof.presume_cmd a b c)));
 
 val _ =
   Outer_Syntax.command @{command_keyword def} "local definition (non-polymorphic)"
@@ -734,7 +792,7 @@
 
 val _ =
   Outer_Syntax.command @{command_keyword write} "add concrete syntax for constants / fixed variables"
-    (opt_mode -- Parse.and_list1 (Parse.const -- Parse.mixfix)
+    (Parse.syntax_mode -- Parse.and_list1 (Parse.const -- Parse.mixfix)
     >> (fn (mode, args) => Toplevel.proof (Proof.write_cmd mode args)));
 
 val _ =
@@ -745,8 +803,13 @@
           --| @{keyword ")"}) ||
         Parse.position Parse.xname >> rpair []) >> (Toplevel.proof o Proof.case_cmd));
 
+in end\<close>
 
-(* proof structure *)
+
+subsubsection \<open>Proof structure\<close>
+
+ML \<open>
+local
 
 val _ =
   Outer_Syntax.command @{command_keyword "{"} "begin explicit proof block"
@@ -760,8 +823,13 @@
   Outer_Syntax.command @{command_keyword next} "enter next proof block"
     (Scan.succeed (Toplevel.proof Proof.next_block));
 
+in end\<close>
 
-(* end proof *)
+
+subsubsection \<open>End proof\<close>
+
+ML \<open>
+local
 
 val _ =
   Outer_Syntax.command @{command_keyword qed} "conclude proof"
@@ -800,8 +868,13 @@
   Outer_Syntax.command @{command_keyword oops} "forget proof"
     (Scan.succeed (Toplevel.forget_proof true));
 
+in end\<close>
 
-(* proof steps *)
+
+subsubsection \<open>Proof steps\<close>
+
+ML \<open>
+local
 
 val _ =
   Outer_Syntax.command @{command_keyword defer} "shuffle internal proof state"
@@ -824,9 +897,12 @@
     (Scan.option Method.parse >> (fn m =>
       (Option.map Method.report m; Toplevel.proofs (Proof.proof m))));
 
+in end\<close>
 
-(* subgoal focus *)
 
+subsubsection \<open>Subgoal focus\<close>
+
+ML \<open>
 local
 
 val opt_fact_binding =
@@ -840,8 +916,6 @@
         (Scan.repeat1 (Parse.position (Parse.maybe Parse.name)))))
     (false, []);
 
-in
-
 val _ =
   Outer_Syntax.command @{command_keyword subgoal}
     "focus on first subgoal within backward refinement"
@@ -849,10 +923,13 @@
       for_params >> (fn ((a, b), c) =>
         Toplevel.proofs (Seq.make_results o Seq.single o #2 o Subgoal.subgoal_cmd a b c)));
 
-end;
+in end\<close>
 
 
-(* calculation *)
+subsubsection \<open>Calculation\<close>
+
+ML \<open>
+local
 
 val calculation_args =
   Scan.option (@{keyword "("} |-- Parse.!!! ((Parse.xthms1 --| @{keyword ")"})));
@@ -879,8 +956,13 @@
   Outer_Syntax.command @{command_keyword print_trans_rules} "print transitivity rules"
     (Scan.succeed (Toplevel.keep (Calculation.print_rules o Toplevel.context_of)));
 
+in end\<close>
 
-(* proof navigation *)
+
+subsubsection \<open>Proof navigation\<close>
+
+ML \<open>
+local
 
 fun report_back () =
   Output.report [Markup.markup Markup.bad "Explicit backtracking"];
@@ -891,9 +973,13 @@
      (Toplevel.actual_proof (fn prf => (report_back (); Proof_Node.back prf)) o
       Toplevel.skip_proof report_back));
 
+in end\<close>
 
 
-(** diagnostic commands (for interactive mode only) **)
+subsection \<open>Diagnostic commands (for interactive mode only)\<close>
+
+ML \<open>
+local
 
 val opt_modes =
   Scan.optional (@{keyword "("} |-- Parse.!!! (Scan.repeat1 Parse.xname --| @{keyword ")"})) [];
@@ -1087,34 +1173,33 @@
     (Scan.repeat1 Parse.path >> (fn names =>
       Toplevel.keep (fn _ => ignore (Present.display_drafts (map Path.explode names)))));
 
+in end\<close>
 
-(* deps *)
 
+subsection \<open>Dependencies\<close>
+
+ML \<open>
 local
-  val theory_bounds =
-    Parse.position Parse.theory_xname >> single ||
-    (@{keyword "("} |-- Parse.enum "|" (Parse.position Parse.theory_xname) --| @{keyword ")"});
-in
+
+val theory_bounds =
+  Parse.position Parse.theory_xname >> single ||
+  (@{keyword "("} |-- Parse.enum "|" (Parse.position Parse.theory_xname) --| @{keyword ")"});
 
 val _ =
   Outer_Syntax.command @{command_keyword thy_deps} "visualize theory dependencies"
     (Scan.option theory_bounds -- Scan.option theory_bounds >>
       (fn args => Toplevel.keep (fn st => Thy_Deps.thy_deps_cmd (Toplevel.context_of st) args)));
 
-end;
 
-local
-  val class_bounds =
-    Parse.sort >> single ||
-    (@{keyword "("} |-- Parse.enum "|" Parse.sort --| @{keyword ")"});
-in
+val class_bounds =
+  Parse.sort >> single ||
+  (@{keyword "("} |-- Parse.enum "|" Parse.sort --| @{keyword ")"});
 
 val _ =
   Outer_Syntax.command @{command_keyword class_deps} "visualize class dependencies"
     (Scan.option class_bounds -- Scan.option class_bounds >> (fn args =>
       Toplevel.keep (fn st => Class_Deps.class_deps_cmd (Toplevel.context_of st) args)));
 
-end;
 
 val _ =
   Outer_Syntax.command @{command_keyword thm_deps} "visualize theorem dependencies"
@@ -1123,10 +1208,9 @@
         Thm_Deps.thm_deps (Toplevel.theory_of st)
           (Attrib.eval_thms (Toplevel.context_of st) args))));
 
-local
-  val thy_names =
-    Scan.repeat1 (Scan.unless Parse.minus (Parse.position Parse.theory_xname));
-in
+
+val thy_names =
+  Scan.repeat1 (Scan.unless Parse.minus (Parse.position Parse.theory_xname));
 
 val _ =
   Outer_Syntax.command @{command_keyword unused_thms} "find unused theorems"
@@ -1146,10 +1230,13 @@
             |> map pretty_thm |> Pretty.writeln_chunks
           end)));
 
-end;
+in end\<close>
 
 
-(* find *)
+subsubsection \<open>Find consts and theorems\<close>
+
+ML \<open>
+local
 
 val _ =
   Outer_Syntax.command @{command_keyword find_consts}
@@ -1158,14 +1245,12 @@
       Toplevel.keep (fn st =>
         Pretty.writeln (Find_Consts.pretty_consts (Toplevel.context_of st) spec))));
 
-local
-  val options =
-    Scan.optional
-      (Parse.$$$ "(" |--
-        Parse.!!! (Scan.option Parse.nat --
-          Scan.optional (Parse.reserved "with_dups" >> K false) true --| Parse.$$$ ")"))
-      (NONE, true);
-in
+val options =
+  Scan.optional
+    (Parse.$$$ "(" |--
+      Parse.!!! (Scan.option Parse.nat --
+        Scan.optional (Parse.reserved "with_dups" >> K false) true --| Parse.$$$ ")"))
+    (NONE, true);
 
 val _ =
   Outer_Syntax.command @{command_keyword find_theorems}
@@ -1175,11 +1260,26 @@
         Pretty.writeln
           (Find_Theorems.pretty_theorems (Find_Theorems.proof_state st) opt_lim rem_dups spec))));
 
-end;
+in end\<close>
 
 
+subsection \<open>Code generation\<close>
 
-(** extraction of programs from proofs **)
+ML \<open>
+local
+
+val _ =
+  Outer_Syntax.command @{command_keyword code_datatype}
+    "define set of code datatype constructors"
+    (Scan.repeat1 Parse.term >> (Toplevel.theory o Code.add_datatype_cmd));
+
+in end\<close>
+
+
+subsection \<open>Extraction of programs from proofs\<close>
+
+ML \<open>
+local
 
 val parse_vars = Scan.optional (Parse.$$$ "(" |-- Parse.list1 Parse.name --| Parse.$$$ ")") [];
 
@@ -1205,21 +1305,10 @@
     (Scan.repeat1 (Parse.xname -- parse_vars) >> (fn xs => Toplevel.theory (fn thy =>
       Extraction.extract (map (apfst (Global_Theory.get_thm thy)) xs) thy)));
 
+in end\<close>
 
 
-(** end **)
-
-val _ =
-  Outer_Syntax.command @{command_keyword end} "end context"
-    (Scan.succeed
-      (Toplevel.exit o Toplevel.end_local_theory o Toplevel.close_target o
-        Toplevel.end_proof (K Proof.end_notepad)));
-
-in end;
-\<close>
-
-
-section \<open>Basic attributes\<close>
+section \<open>Isar attributes\<close>
 
 attribute_setup tagged =
   \<open>Scan.lift (Args.name -- Args.name) >> Thm.tag\<close>