src/Pure/pure_syn.ML
author wenzelm
Sat Nov 04 15:24:40 2017 +0100 (19 months ago)
changeset 67003 49850a679c2c
parent 64556 851ae0e7b09c
child 67381 146757999c8d
permissions -rw-r--r--
more robust sorted_entries;
     1 (*  Title:      Pure/pure_syn.ML
     2     Author:     Makarius
     3 
     4 Outer syntax for bootstrapping: commands that are accessible outside a
     5 regular theory context.
     6 *)
     7 
     8 signature PURE_SYN =
     9 sig
    10   val bootstrap_thy: theory
    11 end;
    12 
    13 structure Pure_Syn: PURE_SYN =
    14 struct
    15 
    16 val semi = Scan.option (Parse.$$$ ";");
    17 
    18 val _ =
    19   Outer_Syntax.command ("chapter", \<^here>) "chapter heading"
    20     (Parse.opt_target -- Parse.document_source --| semi
    21       >> Thy_Output.document_command {markdown = false});
    22 
    23 val _ =
    24   Outer_Syntax.command ("section", \<^here>) "section heading"
    25     (Parse.opt_target -- Parse.document_source --| semi
    26       >> Thy_Output.document_command {markdown = false});
    27 
    28 val _ =
    29   Outer_Syntax.command ("subsection", \<^here>) "subsection heading"
    30     (Parse.opt_target -- Parse.document_source --| semi
    31       >> Thy_Output.document_command {markdown = false});
    32 
    33 val _ =
    34   Outer_Syntax.command ("subsubsection", \<^here>) "subsubsection heading"
    35     (Parse.opt_target -- Parse.document_source --| semi
    36       >> Thy_Output.document_command {markdown = false});
    37 
    38 val _ =
    39   Outer_Syntax.command ("paragraph", \<^here>) "paragraph heading"
    40     (Parse.opt_target -- Parse.document_source --| semi
    41       >> Thy_Output.document_command {markdown = false});
    42 
    43 val _ =
    44   Outer_Syntax.command ("subparagraph", \<^here>) "subparagraph heading"
    45     (Parse.opt_target -- Parse.document_source --| semi
    46       >> Thy_Output.document_command {markdown = false});
    47 
    48 val _ =
    49   Outer_Syntax.command ("text", \<^here>) "formal comment (primary style)"
    50     (Parse.opt_target -- Parse.document_source >> Thy_Output.document_command {markdown = true});
    51 
    52 val _ =
    53   Outer_Syntax.command ("txt", \<^here>) "formal comment (secondary style)"
    54     (Parse.opt_target -- Parse.document_source >> Thy_Output.document_command {markdown = true});
    55 
    56 val _ =
    57   Outer_Syntax.command ("text_raw", \<^here>) "LaTeX text (without surrounding environment)"
    58     (Parse.opt_target -- Parse.document_source >> Thy_Output.document_command {markdown = true});
    59 
    60 val _ =
    61   Outer_Syntax.command ("theory", \<^here>) "begin theory"
    62     (Thy_Header.args >>
    63       (fn _ => Toplevel.init_theory (fn () => error "Missing theory initialization")));
    64 
    65 
    66 val bootstrap_thy = Context.the_global_context ();
    67 
    68 val _ = Theory.setup (Config.put_global Outer_Syntax.bootstrap false);
    69 
    70 end;