src/Pure/pure_syn.ML
author wenzelm
Thu Aug 15 16:02:47 2019 +0200 (9 months ago)
changeset 70533 031620901fcd
parent 69965 da5e7278286b
permissions -rw-r--r--
support for (fully reconstructed) proof terms in Scala;
proper cache_typs;
     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 document_command: {markdown: bool} -> (xstring * Position.T) option * Input.source ->
    11     Toplevel.transition -> Toplevel.transition
    12   val bootstrap_thy: theory
    13 end;
    14 
    15 structure Pure_Syn: PURE_SYN =
    16 struct
    17 
    18 val semi = Scan.option (Parse.$$$ ";");
    19 
    20 fun output_document state markdown txt =
    21   let
    22     val ctxt = Toplevel.presentation_context state;
    23     val pos = Input.pos_of txt;
    24     val _ =
    25       Context_Position.reports ctxt
    26         [(pos, Markup.language_document (Input.is_delimited txt)),
    27          (pos, Markup.plain_text)];
    28   in Thy_Output.output_document ctxt markdown txt end;
    29 
    30 fun document_command markdown (loc, txt) =
    31   Toplevel.keep (fn state =>
    32     (case loc of
    33       NONE => ignore (output_document state markdown txt)
    34     | SOME (_, pos) =>
    35         error ("Illegal target specification -- not a theory context" ^ Position.here pos))) o
    36   Toplevel.present_local_theory loc (fn state =>
    37     ignore (output_document state markdown txt));
    38 
    39 val _ =
    40   Outer_Syntax.command ("chapter", \<^here>) "chapter heading"
    41     (Parse.opt_target -- Parse.document_source --| semi >> document_command {markdown = false});
    42 
    43 val _ =
    44   Outer_Syntax.command ("section", \<^here>) "section heading"
    45     (Parse.opt_target -- Parse.document_source --| semi >> document_command {markdown = false});
    46 
    47 val _ =
    48   Outer_Syntax.command ("subsection", \<^here>) "subsection heading"
    49     (Parse.opt_target -- Parse.document_source --| semi >> document_command {markdown = false});
    50 
    51 val _ =
    52   Outer_Syntax.command ("subsubsection", \<^here>) "subsubsection heading"
    53     (Parse.opt_target -- Parse.document_source --| semi >> document_command {markdown = false});
    54 
    55 val _ =
    56   Outer_Syntax.command ("paragraph", \<^here>) "paragraph heading"
    57     (Parse.opt_target -- Parse.document_source --| semi >> document_command {markdown = false});
    58 
    59 val _ =
    60   Outer_Syntax.command ("subparagraph", \<^here>) "subparagraph heading"
    61     (Parse.opt_target -- Parse.document_source --| semi >> document_command {markdown = false});
    62 
    63 val _ =
    64   Outer_Syntax.command ("text", \<^here>) "formal comment (primary style)"
    65     (Parse.opt_target -- Parse.document_source >> document_command {markdown = true});
    66 
    67 val _ =
    68   Outer_Syntax.command ("txt", \<^here>) "formal comment (secondary style)"
    69     (Parse.opt_target -- Parse.document_source >> document_command {markdown = true});
    70 
    71 val _ =
    72   Outer_Syntax.command ("text_raw", \<^here>) "LaTeX text (without surrounding environment)"
    73     (Parse.opt_target -- Parse.document_source >> document_command {markdown = true});
    74 
    75 val _ =
    76   Outer_Syntax.command ("theory", \<^here>) "begin theory"
    77     (Thy_Header.args >>
    78       (fn _ => Toplevel.init_theory (fn () => error "Missing theory initialization")));
    79 
    80 
    81 val bootstrap_thy = Context.the_global_context ();
    82 
    83 val _ = Theory.setup (Config.put_global Outer_Syntax.bootstrap false);
    84 
    85 end;