# 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 \ (@@{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} \} \<^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)"