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;
wenzelm@48879
     1
(*  Title:      Pure/pure_syn.ML
wenzelm@48879
     2
    Author:     Makarius
wenzelm@48879
     3
wenzelm@60096
     4
Outer syntax for bootstrapping: commands that are accessible outside a
wenzelm@60096
     5
regular theory context.
wenzelm@48879
     6
*)
wenzelm@48879
     7
wenzelm@60095
     8
signature PURE_SYN =
wenzelm@60095
     9
sig
wenzelm@67381
    10
  val document_command: {markdown: bool} -> (xstring * Position.T) option * Input.source ->
wenzelm@67381
    11
    Toplevel.transition -> Toplevel.transition
wenzelm@60095
    12
  val bootstrap_thy: theory
wenzelm@60095
    13
end;
wenzelm@60095
    14
wenzelm@60095
    15
structure Pure_Syn: PURE_SYN =
wenzelm@48879
    16
struct
wenzelm@48879
    17
wenzelm@62912
    18
val semi = Scan.option (Parse.$$$ ";");
wenzelm@62912
    19
wenzelm@67569
    20
fun output_document state markdown txt =
wenzelm@67569
    21
  let
wenzelm@67569
    22
    val ctxt = Toplevel.presentation_context state;
wenzelm@69965
    23
    val pos = Input.pos_of txt;
wenzelm@67569
    24
    val _ =
wenzelm@69965
    25
      Context_Position.reports ctxt
wenzelm@69965
    26
        [(pos, Markup.language_document (Input.is_delimited txt)),
wenzelm@69965
    27
         (pos, Markup.plain_text)];
wenzelm@67569
    28
  in Thy_Output.output_document ctxt markdown txt end;
wenzelm@67569
    29
wenzelm@67569
    30
fun document_command markdown (loc, txt) =
wenzelm@67381
    31
  Toplevel.keep (fn state =>
wenzelm@67381
    32
    (case loc of
wenzelm@67569
    33
      NONE => ignore (output_document state markdown txt)
wenzelm@67381
    34
    | SOME (_, pos) =>
wenzelm@67381
    35
        error ("Illegal target specification -- not a theory context" ^ Position.here pos))) o
wenzelm@67381
    36
  Toplevel.present_local_theory loc (fn state =>
wenzelm@67569
    37
    ignore (output_document state markdown txt));
wenzelm@67381
    38
wenzelm@58928
    39
val _ =
wenzelm@64556
    40
  Outer_Syntax.command ("chapter", \<^here>) "chapter heading"
wenzelm@67381
    41
    (Parse.opt_target -- Parse.document_source --| semi >> document_command {markdown = false});
wenzelm@58999
    42
wenzelm@58999
    43
val _ =
wenzelm@64556
    44
  Outer_Syntax.command ("section", \<^here>) "section heading"
wenzelm@67381
    45
    (Parse.opt_target -- Parse.document_source --| semi >> document_command {markdown = false});
wenzelm@58918
    46
wenzelm@48879
    47
val _ =
wenzelm@64556
    48
  Outer_Syntax.command ("subsection", \<^here>) "subsection heading"
wenzelm@67381
    49
    (Parse.opt_target -- Parse.document_source --| semi >> document_command {markdown = false});
wenzelm@58999
    50
wenzelm@58999
    51
val _ =
wenzelm@64556
    52
  Outer_Syntax.command ("subsubsection", \<^here>) "subsubsection heading"
wenzelm@67381
    53
    (Parse.opt_target -- Parse.document_source --| semi >> document_command {markdown = false});
wenzelm@58928
    54
wenzelm@58928
    55
val _ =
wenzelm@64556
    56
  Outer_Syntax.command ("paragraph", \<^here>) "paragraph heading"
wenzelm@67381
    57
    (Parse.opt_target -- Parse.document_source --| semi >> document_command {markdown = false});
wenzelm@61463
    58
wenzelm@61463
    59
val _ =
wenzelm@64556
    60
  Outer_Syntax.command ("subparagraph", \<^here>) "subparagraph heading"
wenzelm@67381
    61
    (Parse.opt_target -- Parse.document_source --| semi >> document_command {markdown = false});
wenzelm@61463
    62
wenzelm@61463
    63
val _ =
wenzelm@64556
    64
  Outer_Syntax.command ("text", \<^here>) "formal comment (primary style)"
wenzelm@67381
    65
    (Parse.opt_target -- Parse.document_source >> document_command {markdown = true});
wenzelm@58928
    66
wenzelm@58928
    67
val _ =
wenzelm@64556
    68
  Outer_Syntax.command ("txt", \<^here>) "formal comment (secondary style)"
wenzelm@67381
    69
    (Parse.opt_target -- Parse.document_source >> document_command {markdown = true});
wenzelm@58999
    70
wenzelm@58999
    71
val _ =
wenzelm@64556
    72
  Outer_Syntax.command ("text_raw", \<^here>) "LaTeX text (without surrounding environment)"
wenzelm@67381
    73
    (Parse.opt_target -- Parse.document_source >> document_command {markdown = true});
wenzelm@58928
    74
wenzelm@58928
    75
val _ =
wenzelm@64556
    76
  Outer_Syntax.command ("theory", \<^here>) "begin theory"
wenzelm@58852
    77
    (Thy_Header.args >>
wenzelm@58852
    78
      (fn _ => Toplevel.init_theory (fn () => error "Missing theory initialization")));
wenzelm@48879
    79
wenzelm@60095
    80
wenzelm@62876
    81
val bootstrap_thy = Context.the_global_context ();
wenzelm@60095
    82
wenzelm@60095
    83
val _ = Theory.setup (Config.put_global Outer_Syntax.bootstrap false);
wenzelm@60095
    84
wenzelm@48879
    85
end;