# HG changeset patch
# User wenzelm
# Date 1460059763 -7200
# Node ID 745d31e63c21b80278a8a4315bb23ee18c78b8f4
# Parent  78e03d8bf1c4d85178924e26687b02c3dc2067c5
section headings for ROOT.ML;

diff -r 78e03d8bf1c4 -r 745d31e63c21 src/Doc/Isar_Ref/Document_Preparation.thy
--- 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
diff -r 78e03d8bf1c4 -r 745d31e63c21 src/Pure/ML/ml_name_space.ML
--- 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"];
diff -r 78e03d8bf1c4 -r 745d31e63c21 src/Pure/ROOT.ML
--- 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";
diff -r 78e03d8bf1c4 -r 745d31e63c21 src/Pure/Tools/ml_process.scala
--- 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)
diff -r 78e03d8bf1c4 -r 745d31e63c21 src/Pure/pure_syn.ML
--- 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)"