--- a/src/Doc/Isar_Ref/Document_Preparation.thy Thu Apr 07 21:39:03 2016 +0200
+++ b/src/Doc/Isar_Ref/Document_Preparation.thy Thu Apr 07 22:09:23 2016 +0200
@@ -49,8 +49,9 @@
@{rail \<open>
(@@{command chapter} | @@{command section} | @@{command subsection} |
- @@{command subsubsection} | @@{command paragraph} | @@{command subparagraph} |
- @@{command text} | @@{command txt} | @@{command text_raw}) @{syntax text}
+ @@{command subsubsection} | @@{command paragraph} | @@{command subparagraph})
+ @{syntax text} ';'? |
+ (@@{command text} | @@{command txt} | @@{command text_raw}) @{syntax text}
\<close>}
\<^descr> @{command chapter}, @{command section}, @{command subsection} etc.\ mark
--- a/src/Pure/ML/ml_name_space.ML Thu Apr 07 21:39:03 2016 +0200
+++ b/src/Pure/ML/ml_name_space.ML Thu Apr 07 22:09:23 2016 +0200
@@ -61,7 +61,8 @@
(* bootstrap environment *)
val bootstrap_values =
- ["use", "exit", "ML_file", "ML_system_pretty", "ML_system_pp", "ML_system_overload"];
+ ["use", "exit", "ML_file", "ML_system_pretty", "ML_system_pp", "ML_system_overload",
+ "chapter", "section", "subsection", "subsubsection", "paragraph", "subparagraph"];
val bootstrap_structures =
["PolyML", "CInterface", "Foreign", "RunCall", "RuntimeCalls", "Signal", "Thread_Data",
"ML_Recursive"];
--- a/src/Pure/ROOT.ML Thu Apr 07 21:39:03 2016 +0200
+++ b/src/Pure/ROOT.ML Thu Apr 07 22:09:23 2016 +0200
@@ -1,9 +1,9 @@
-(*** Isabelle/Pure bootstrap ***)
+chapter "Isabelle/Pure bootstrap";
ML_file "ML/ml_name_space.ML";
-(** bootstrap phase 0: Poly/ML setup **)
+section "Bootstrap phase 0: Poly/ML setup";
ML_file "ML/ml_pervasive0.ML";
ML_file "ML/ml_system.ML";
@@ -22,10 +22,9 @@
ML_file_no_debug "ML/ml_debugger.ML";
+section "Bootstrap phase 1: towards ML within position context";
-(** bootstrap phase 1: towards ML within position context *)
-
-(* library of general tools *)
+subsection "Library of general tools";
ML_file "General/basics.ML";
ML_file "library.ML";
@@ -51,9 +50,9 @@
ML_file "ML/ml_compiler1.ML";
-(** bootstrap phase 2: towards ML within Isar context *)
+section "Bootstrap phase 2: towards ML within Isar context";
-(* library of general tools *)
+subsection "Library of general tools";
ML_file "General/integer.ML";
ML_file "General/stack.ML";
@@ -83,7 +82,7 @@
ML_file "General/graph.ML";
-(* fundamental structures *)
+subsection "Fundamental structures";
ML_file "name.ML";
ML_file "term.ML";
@@ -93,7 +92,7 @@
ML_file "config.ML";
-(* concurrency within the ML runtime *)
+subsection "Concurrency within the ML runtime";
ML_file "ML/exn_properties.ML";
@@ -117,7 +116,7 @@
ML_file "PIDE/active.ML";
-(* inner syntax *)
+subsection "Inner syntax";
ML_file "Syntax/type_annotation.ML";
ML_file "Syntax/term_position.ML";
@@ -131,7 +130,7 @@
ML_file "Syntax/syntax.ML";
-(* core of tactical proof system *)
+subsection "Core of tactical proof system";
ML_file "term_ord.ML";
ML_file "term_subst.ML";
@@ -174,7 +173,7 @@
ML_file "assumption.ML";
-(* Isar -- Intelligible Semi-Automated Reasoning *)
+subsection "Isar -- Intelligible Semi-Automated Reasoning";
(*ML support and global execution*)
ML_file "ML/ml_syntax.ML";
@@ -221,8 +220,7 @@
ML_file "ML/ml_compiler2.ML";
-
-(** bootstrap phase 3: towards theory "Pure" and final ML toplevel setup *)
+section "Bootstrap phase 3: towards theory Pure and final ML toplevel setup";
(*basic proof engine*)
ML_file "par_tactical.ML";
@@ -297,7 +295,7 @@
ML_file "Isar/isar_cmd.ML";
-(* Isabelle/Isar system *)
+subsection "Isabelle/Isar system";
ML_file "System/command_line.ML";
ML_file "System/system_channel.ML";
@@ -307,7 +305,7 @@
ML_file "PIDE/protocol.ML";
-(* miscellaneous tools and packages for Pure Isabelle *)
+subsection "Miscellaneous tools and packages for Pure Isabelle";
ML_file "ML/ml_pp.ML";
ML_file "ML/ml_antiquotations.ML";
--- a/src/Pure/Tools/ml_process.scala Thu Apr 07 21:39:03 2016 +0200
+++ b/src/Pure/Tools/ml_process.scala Thu Apr 07 22:09:23 2016 +0200
@@ -39,7 +39,15 @@
val eval_init =
if (heaps.isEmpty) {
List(
- "val ML_file = PolyML.use",
+ """
+ fun chapter (_: string) = ();
+ fun section (_: string) = ();
+ fun subsection (_: string) = ();
+ fun subsubsection (_: string) = ();
+ fun paragraph (_: string) = ();
+ fun subparagraph (_: string) = ();
+ val ML_file = PolyML.use;
+ """,
if (Isabelle_System.getenv("ML_SYSTEM") == "polyml-5.6") "structure FixedInt = IntInf"
else "",
if (Platform.is_windows)
--- a/src/Pure/pure_syn.ML Thu Apr 07 21:39:03 2016 +0200
+++ b/src/Pure/pure_syn.ML Thu Apr 07 22:09:23 2016 +0200
@@ -13,29 +13,37 @@
structure Pure_Syn: PURE_SYN =
struct
+val semi = Scan.option (Parse.$$$ ";");
+
val _ =
Outer_Syntax.command ("chapter", @{here}) "chapter heading"
- (Parse.opt_target -- Parse.document_source >> Thy_Output.document_command {markdown = false});
+ (Parse.opt_target -- Parse.document_source --| semi
+ >> Thy_Output.document_command {markdown = false});
val _ =
Outer_Syntax.command ("section", @{here}) "section heading"
- (Parse.opt_target -- Parse.document_source >> Thy_Output.document_command {markdown = false});
+ (Parse.opt_target -- Parse.document_source --| semi
+ >> Thy_Output.document_command {markdown = false});
val _ =
Outer_Syntax.command ("subsection", @{here}) "subsection heading"
- (Parse.opt_target -- Parse.document_source >> Thy_Output.document_command {markdown = false});
+ (Parse.opt_target -- Parse.document_source --| semi
+ >> Thy_Output.document_command {markdown = false});
val _ =
Outer_Syntax.command ("subsubsection", @{here}) "subsubsection heading"
- (Parse.opt_target -- Parse.document_source >> Thy_Output.document_command {markdown = false});
+ (Parse.opt_target -- Parse.document_source --| semi
+ >> Thy_Output.document_command {markdown = false});
val _ =
Outer_Syntax.command ("paragraph", @{here}) "paragraph heading"
- (Parse.opt_target -- Parse.document_source >> Thy_Output.document_command {markdown = false});
+ (Parse.opt_target -- Parse.document_source --| semi
+ >> Thy_Output.document_command {markdown = false});
val _ =
Outer_Syntax.command ("subparagraph", @{here}) "subparagraph heading"
- (Parse.opt_target -- Parse.document_source >> Thy_Output.document_command {markdown = false});
+ (Parse.opt_target -- Parse.document_source --| semi
+ >> Thy_Output.document_command {markdown = false});
val _ =
Outer_Syntax.command ("text", @{here}) "formal comment (primary style)"