src/Pure/pure_syn.ML
author wenzelm
Tue, 05 Apr 2016 20:03:24 +0200
changeset 62876 507c90523113
parent 62453 b93cc7d73431
child 62912 745d31e63c21
permissions -rw-r--r--
clarified modules -- simplified bootstrap;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
48879
cb5cdbb645cd clarified bootstrapping of Pure;
wenzelm
parents:
diff changeset
     1
(*  Title:      Pure/pure_syn.ML
cb5cdbb645cd clarified bootstrapping of Pure;
wenzelm
parents:
diff changeset
     2
    Author:     Makarius
cb5cdbb645cd clarified bootstrapping of Pure;
wenzelm
parents:
diff changeset
     3
60096
7b98dbc1d13e tuned comment;
wenzelm
parents: 60095
diff changeset
     4
Outer syntax for bootstrapping: commands that are accessible outside a
7b98dbc1d13e tuned comment;
wenzelm
parents: 60095
diff changeset
     5
regular theory context.
48879
cb5cdbb645cd clarified bootstrapping of Pure;
wenzelm
parents:
diff changeset
     6
*)
cb5cdbb645cd clarified bootstrapping of Pure;
wenzelm
parents:
diff changeset
     7
60095
35f626b11422 more explicit bootstrap_thy;
wenzelm
parents: 58999
diff changeset
     8
signature PURE_SYN =
35f626b11422 more explicit bootstrap_thy;
wenzelm
parents: 58999
diff changeset
     9
sig
35f626b11422 more explicit bootstrap_thy;
wenzelm
parents: 58999
diff changeset
    10
  val bootstrap_thy: theory
35f626b11422 more explicit bootstrap_thy;
wenzelm
parents: 58999
diff changeset
    11
end;
35f626b11422 more explicit bootstrap_thy;
wenzelm
parents: 58999
diff changeset
    12
35f626b11422 more explicit bootstrap_thy;
wenzelm
parents: 58999
diff changeset
    13
structure Pure_Syn: PURE_SYN =
48879
cb5cdbb645cd clarified bootstrapping of Pure;
wenzelm
parents:
diff changeset
    14
struct
cb5cdbb645cd clarified bootstrapping of Pure;
wenzelm
parents:
diff changeset
    15
58928
23d0ffd48006 plain value Keywords.keywords, which might be used outside theory for bootstrap purposes;
wenzelm
parents: 58918
diff changeset
    16
val _ =
58999
ed09ae4ea2d8 uniform treatment of all document markup commands: 'text' and 'txt' merely differ in LaTeX style;
wenzelm
parents: 58928
diff changeset
    17
  Outer_Syntax.command ("chapter", @{here}) "chapter heading"
61457
3e21699bb83b clarified Antiquote.antiq_reports;
wenzelm
parents: 61036
diff changeset
    18
    (Parse.opt_target -- Parse.document_source >> Thy_Output.document_command {markdown = false});
58999
ed09ae4ea2d8 uniform treatment of all document markup commands: 'text' and 'txt' merely differ in LaTeX style;
wenzelm
parents: 58928
diff changeset
    19
ed09ae4ea2d8 uniform treatment of all document markup commands: 'text' and 'txt' merely differ in LaTeX style;
wenzelm
parents: 58928
diff changeset
    20
val _ =
ed09ae4ea2d8 uniform treatment of all document markup commands: 'text' and 'txt' merely differ in LaTeX style;
wenzelm
parents: 58928
diff changeset
    21
  Outer_Syntax.command ("section", @{here}) "section heading"
61457
3e21699bb83b clarified Antiquote.antiq_reports;
wenzelm
parents: 61036
diff changeset
    22
    (Parse.opt_target -- Parse.document_source >> Thy_Output.document_command {markdown = false});
58918
8d36bc5eaed3 simplified keyword kinds;
wenzelm
parents: 58852
diff changeset
    23
48879
cb5cdbb645cd clarified bootstrapping of Pure;
wenzelm
parents:
diff changeset
    24
val _ =
58999
ed09ae4ea2d8 uniform treatment of all document markup commands: 'text' and 'txt' merely differ in LaTeX style;
wenzelm
parents: 58928
diff changeset
    25
  Outer_Syntax.command ("subsection", @{here}) "subsection heading"
61457
3e21699bb83b clarified Antiquote.antiq_reports;
wenzelm
parents: 61036
diff changeset
    26
    (Parse.opt_target -- Parse.document_source >> Thy_Output.document_command {markdown = false});
58999
ed09ae4ea2d8 uniform treatment of all document markup commands: 'text' and 'txt' merely differ in LaTeX style;
wenzelm
parents: 58928
diff changeset
    27
ed09ae4ea2d8 uniform treatment of all document markup commands: 'text' and 'txt' merely differ in LaTeX style;
wenzelm
parents: 58928
diff changeset
    28
val _ =
ed09ae4ea2d8 uniform treatment of all document markup commands: 'text' and 'txt' merely differ in LaTeX style;
wenzelm
parents: 58928
diff changeset
    29
  Outer_Syntax.command ("subsubsection", @{here}) "subsubsection heading"
61457
3e21699bb83b clarified Antiquote.antiq_reports;
wenzelm
parents: 61036
diff changeset
    30
    (Parse.opt_target -- Parse.document_source >> Thy_Output.document_command {markdown = false});
58928
23d0ffd48006 plain value Keywords.keywords, which might be used outside theory for bootstrap purposes;
wenzelm
parents: 58918
diff changeset
    31
23d0ffd48006 plain value Keywords.keywords, which might be used outside theory for bootstrap purposes;
wenzelm
parents: 58918
diff changeset
    32
val _ =
61463
8e46cea6a45a added 'paragraph', 'subparagraph';
wenzelm
parents: 61457
diff changeset
    33
  Outer_Syntax.command ("paragraph", @{here}) "paragraph heading"
8e46cea6a45a added 'paragraph', 'subparagraph';
wenzelm
parents: 61457
diff changeset
    34
    (Parse.opt_target -- Parse.document_source >> Thy_Output.document_command {markdown = false});
8e46cea6a45a added 'paragraph', 'subparagraph';
wenzelm
parents: 61457
diff changeset
    35
8e46cea6a45a added 'paragraph', 'subparagraph';
wenzelm
parents: 61457
diff changeset
    36
val _ =
8e46cea6a45a added 'paragraph', 'subparagraph';
wenzelm
parents: 61457
diff changeset
    37
  Outer_Syntax.command ("subparagraph", @{here}) "subparagraph heading"
8e46cea6a45a added 'paragraph', 'subparagraph';
wenzelm
parents: 61457
diff changeset
    38
    (Parse.opt_target -- Parse.document_source >> Thy_Output.document_command {markdown = false});
8e46cea6a45a added 'paragraph', 'subparagraph';
wenzelm
parents: 61457
diff changeset
    39
8e46cea6a45a added 'paragraph', 'subparagraph';
wenzelm
parents: 61457
diff changeset
    40
val _ =
58999
ed09ae4ea2d8 uniform treatment of all document markup commands: 'text' and 'txt' merely differ in LaTeX style;
wenzelm
parents: 58928
diff changeset
    41
  Outer_Syntax.command ("text", @{here}) "formal comment (primary style)"
61457
3e21699bb83b clarified Antiquote.antiq_reports;
wenzelm
parents: 61036
diff changeset
    42
    (Parse.opt_target -- Parse.document_source >> Thy_Output.document_command {markdown = true});
58928
23d0ffd48006 plain value Keywords.keywords, which might be used outside theory for bootstrap purposes;
wenzelm
parents: 58918
diff changeset
    43
23d0ffd48006 plain value Keywords.keywords, which might be used outside theory for bootstrap purposes;
wenzelm
parents: 58918
diff changeset
    44
val _ =
58999
ed09ae4ea2d8 uniform treatment of all document markup commands: 'text' and 'txt' merely differ in LaTeX style;
wenzelm
parents: 58928
diff changeset
    45
  Outer_Syntax.command ("txt", @{here}) "formal comment (secondary style)"
61457
3e21699bb83b clarified Antiquote.antiq_reports;
wenzelm
parents: 61036
diff changeset
    46
    (Parse.opt_target -- Parse.document_source >> Thy_Output.document_command {markdown = true});
58999
ed09ae4ea2d8 uniform treatment of all document markup commands: 'text' and 'txt' merely differ in LaTeX style;
wenzelm
parents: 58928
diff changeset
    47
ed09ae4ea2d8 uniform treatment of all document markup commands: 'text' and 'txt' merely differ in LaTeX style;
wenzelm
parents: 58928
diff changeset
    48
val _ =
61464
d35ff80f27fb more uniform command setup;
wenzelm
parents: 61463
diff changeset
    49
  Outer_Syntax.command ("text_raw", @{here}) "LaTeX text (without surrounding environment)"
d35ff80f27fb more uniform command setup;
wenzelm
parents: 61463
diff changeset
    50
    (Parse.opt_target -- Parse.document_source >> Thy_Output.document_command {markdown = true});
58928
23d0ffd48006 plain value Keywords.keywords, which might be used outside theory for bootstrap purposes;
wenzelm
parents: 58918
diff changeset
    51
23d0ffd48006 plain value Keywords.keywords, which might be used outside theory for bootstrap purposes;
wenzelm
parents: 58918
diff changeset
    52
val _ =
23d0ffd48006 plain value Keywords.keywords, which might be used outside theory for bootstrap purposes;
wenzelm
parents: 58918
diff changeset
    53
  Outer_Syntax.command ("theory", @{here}) "begin theory"
58852
621c052789b4 obsolete;
wenzelm
parents: 58842
diff changeset
    54
    (Thy_Header.args >>
621c052789b4 obsolete;
wenzelm
parents: 58842
diff changeset
    55
      (fn _ => Toplevel.init_theory (fn () => error "Missing theory initialization")));
48879
cb5cdbb645cd clarified bootstrapping of Pure;
wenzelm
parents:
diff changeset
    56
60095
35f626b11422 more explicit bootstrap_thy;
wenzelm
parents: 58999
diff changeset
    57
62876
507c90523113 clarified modules -- simplified bootstrap;
wenzelm
parents: 62453
diff changeset
    58
val bootstrap_thy = Context.the_global_context ();
60095
35f626b11422 more explicit bootstrap_thy;
wenzelm
parents: 58999
diff changeset
    59
35f626b11422 more explicit bootstrap_thy;
wenzelm
parents: 58999
diff changeset
    60
val _ = Theory.setup (Config.put_global Outer_Syntax.bootstrap false);
35f626b11422 more explicit bootstrap_thy;
wenzelm
parents: 58999
diff changeset
    61
48879
cb5cdbb645cd clarified bootstrapping of Pure;
wenzelm
parents:
diff changeset
    62
end;