src/Pure/pure_syn.ML
author wenzelm
Tue Sep 26 20:54:40 2017 +0200 (21 months ago)
changeset 66695 91500c024c7f
parent 64556 851ae0e7b09c
child 67381 146757999c8d
permissions -rw-r--r--
tuned;
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@60095
    10
  val bootstrap_thy: theory
wenzelm@60095
    11
end;
wenzelm@60095
    12
wenzelm@60095
    13
structure Pure_Syn: PURE_SYN =
wenzelm@48879
    14
struct
wenzelm@48879
    15
wenzelm@62912
    16
val semi = Scan.option (Parse.$$$ ";");
wenzelm@62912
    17
wenzelm@58928
    18
val _ =
wenzelm@64556
    19
  Outer_Syntax.command ("chapter", \<^here>) "chapter heading"
wenzelm@62912
    20
    (Parse.opt_target -- Parse.document_source --| semi
wenzelm@62912
    21
      >> Thy_Output.document_command {markdown = false});
wenzelm@58999
    22
wenzelm@58999
    23
val _ =
wenzelm@64556
    24
  Outer_Syntax.command ("section", \<^here>) "section heading"
wenzelm@62912
    25
    (Parse.opt_target -- Parse.document_source --| semi
wenzelm@62912
    26
      >> Thy_Output.document_command {markdown = false});
wenzelm@58918
    27
wenzelm@48879
    28
val _ =
wenzelm@64556
    29
  Outer_Syntax.command ("subsection", \<^here>) "subsection heading"
wenzelm@62912
    30
    (Parse.opt_target -- Parse.document_source --| semi
wenzelm@62912
    31
      >> Thy_Output.document_command {markdown = false});
wenzelm@58999
    32
wenzelm@58999
    33
val _ =
wenzelm@64556
    34
  Outer_Syntax.command ("subsubsection", \<^here>) "subsubsection heading"
wenzelm@62912
    35
    (Parse.opt_target -- Parse.document_source --| semi
wenzelm@62912
    36
      >> Thy_Output.document_command {markdown = false});
wenzelm@58928
    37
wenzelm@58928
    38
val _ =
wenzelm@64556
    39
  Outer_Syntax.command ("paragraph", \<^here>) "paragraph heading"
wenzelm@62912
    40
    (Parse.opt_target -- Parse.document_source --| semi
wenzelm@62912
    41
      >> Thy_Output.document_command {markdown = false});
wenzelm@61463
    42
wenzelm@61463
    43
val _ =
wenzelm@64556
    44
  Outer_Syntax.command ("subparagraph", \<^here>) "subparagraph heading"
wenzelm@62912
    45
    (Parse.opt_target -- Parse.document_source --| semi
wenzelm@62912
    46
      >> Thy_Output.document_command {markdown = false});
wenzelm@61463
    47
wenzelm@61463
    48
val _ =
wenzelm@64556
    49
  Outer_Syntax.command ("text", \<^here>) "formal comment (primary style)"
wenzelm@61457
    50
    (Parse.opt_target -- Parse.document_source >> Thy_Output.document_command {markdown = true});
wenzelm@58928
    51
wenzelm@58928
    52
val _ =
wenzelm@64556
    53
  Outer_Syntax.command ("txt", \<^here>) "formal comment (secondary style)"
wenzelm@61457
    54
    (Parse.opt_target -- Parse.document_source >> Thy_Output.document_command {markdown = true});
wenzelm@58999
    55
wenzelm@58999
    56
val _ =
wenzelm@64556
    57
  Outer_Syntax.command ("text_raw", \<^here>) "LaTeX text (without surrounding environment)"
wenzelm@61464
    58
    (Parse.opt_target -- Parse.document_source >> Thy_Output.document_command {markdown = true});
wenzelm@58928
    59
wenzelm@58928
    60
val _ =
wenzelm@64556
    61
  Outer_Syntax.command ("theory", \<^here>) "begin theory"
wenzelm@58852
    62
    (Thy_Header.args >>
wenzelm@58852
    63
      (fn _ => Toplevel.init_theory (fn () => error "Missing theory initialization")));
wenzelm@48879
    64
wenzelm@60095
    65
wenzelm@62876
    66
val bootstrap_thy = Context.the_global_context ();
wenzelm@60095
    67
wenzelm@60095
    68
val _ = Theory.setup (Config.put_global Outer_Syntax.bootstrap false);
wenzelm@60095
    69
wenzelm@48879
    70
end;