src/Pure/pure_syn.ML
author wenzelm
Mon Feb 23 14:50:30 2015 +0100 (2015-02-23)
changeset 59564 fdc03c8daacc
parent 58999 ed09ae4ea2d8
child 60095 35f626b11422
permissions -rw-r--r--
Goal.prove_multi is superseded by the fully general Goal.prove_common;
wenzelm@48879
     1
(*  Title:      Pure/pure_syn.ML
wenzelm@48879
     2
    Author:     Makarius
wenzelm@48879
     3
wenzelm@58928
     4
Outer syntax for bootstrapping Isabelle/Pure.
wenzelm@48879
     5
*)
wenzelm@48879
     6
wenzelm@48879
     7
structure Pure_Syn: sig end =
wenzelm@48879
     8
struct
wenzelm@48879
     9
wenzelm@58928
    10
val _ =
wenzelm@58999
    11
  Outer_Syntax.command ("header", @{here}) "theory header"
wenzelm@58999
    12
    (Parse.document_source >> Thy_Output.old_header_command);
wenzelm@58918
    13
wenzelm@58928
    14
val _ =
wenzelm@58999
    15
  Outer_Syntax.command ("chapter", @{here}) "chapter heading"
wenzelm@58999
    16
    (Parse.opt_target -- Parse.document_source >> Thy_Output.document_command);
wenzelm@58999
    17
wenzelm@58999
    18
val _ =
wenzelm@58999
    19
  Outer_Syntax.command ("section", @{here}) "section heading"
wenzelm@58999
    20
    (Parse.opt_target -- Parse.document_source >> Thy_Output.document_command);
wenzelm@58918
    21
wenzelm@48879
    22
val _ =
wenzelm@58999
    23
  Outer_Syntax.command ("subsection", @{here}) "subsection heading"
wenzelm@58999
    24
    (Parse.opt_target -- Parse.document_source >> Thy_Output.document_command);
wenzelm@58999
    25
wenzelm@58999
    26
val _ =
wenzelm@58999
    27
  Outer_Syntax.command ("subsubsection", @{here}) "subsubsection heading"
wenzelm@58999
    28
    (Parse.opt_target -- Parse.document_source >> Thy_Output.document_command);
wenzelm@58928
    29
wenzelm@58928
    30
val _ =
wenzelm@58999
    31
  Outer_Syntax.command ("text", @{here}) "formal comment (primary style)"
wenzelm@58999
    32
    (Parse.opt_target -- Parse.document_source >> Thy_Output.document_command);
wenzelm@58928
    33
wenzelm@58928
    34
val _ =
wenzelm@58999
    35
  Outer_Syntax.command ("txt", @{here}) "formal comment (secondary style)"
wenzelm@58999
    36
    (Parse.opt_target -- Parse.document_source >> Thy_Output.document_command);
wenzelm@58999
    37
wenzelm@58999
    38
val _ =
wenzelm@58999
    39
  Outer_Syntax.command ("text_raw", @{here}) "raw LaTeX text"
wenzelm@58999
    40
    (Parse.document_source >> K (Toplevel.imperative I));
wenzelm@58928
    41
wenzelm@58928
    42
val _ =
wenzelm@58928
    43
  Outer_Syntax.command ("theory", @{here}) "begin theory"
wenzelm@58852
    44
    (Thy_Header.args >>
wenzelm@58852
    45
      (fn _ => Toplevel.init_theory (fn () => error "Missing theory initialization")));
wenzelm@48879
    46
wenzelm@48879
    47
end;
wenzelm@48879
    48