src/Pure/pure_syn.ML
author wenzelm
Wed, 19 May 2021 21:42:45 +0200
changeset 73751 fefb5ccb1e5e
parent 69965 da5e7278286b
child 73752 eeb076fc569f
permissions -rw-r--r--
clarified modules;
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
67381
146757999c8d theory Pure is default presentation context;
wenzelm
parents: 64556
diff changeset
    10
  val document_command: {markdown: bool} -> (xstring * Position.T) option * Input.source ->
146757999c8d theory Pure is default presentation context;
wenzelm
parents: 64556
diff changeset
    11
    Toplevel.transition -> Toplevel.transition
60095
35f626b11422 more explicit bootstrap_thy;
wenzelm
parents: 58999
diff changeset
    12
  val bootstrap_thy: theory
35f626b11422 more explicit bootstrap_thy;
wenzelm
parents: 58999
diff changeset
    13
end;
35f626b11422 more explicit bootstrap_thy;
wenzelm
parents: 58999
diff changeset
    14
35f626b11422 more explicit bootstrap_thy;
wenzelm
parents: 58999
diff changeset
    15
structure Pure_Syn: PURE_SYN =
48879
cb5cdbb645cd clarified bootstrapping of Pure;
wenzelm
parents:
diff changeset
    16
struct
cb5cdbb645cd clarified bootstrapping of Pure;
wenzelm
parents:
diff changeset
    17
62912
745d31e63c21 section headings for ROOT.ML;
wenzelm
parents: 62876
diff changeset
    18
val semi = Scan.option (Parse.$$$ ";");
745d31e63c21 section headings for ROOT.ML;
wenzelm
parents: 62876
diff changeset
    19
73751
fefb5ccb1e5e clarified modules;
wenzelm
parents: 69965
diff changeset
    20
val output_document =
fefb5ccb1e5e clarified modules;
wenzelm
parents: 69965
diff changeset
    21
  Thy_Output.output_document_report o Toplevel.presentation_context;
67569
5d71b114e7a3 avoid proliferation of language_document reports;
wenzelm
parents: 67381
diff changeset
    22
5d71b114e7a3 avoid proliferation of language_document reports;
wenzelm
parents: 67381
diff changeset
    23
fun document_command markdown (loc, txt) =
67381
146757999c8d theory Pure is default presentation context;
wenzelm
parents: 64556
diff changeset
    24
  Toplevel.keep (fn state =>
146757999c8d theory Pure is default presentation context;
wenzelm
parents: 64556
diff changeset
    25
    (case loc of
67569
5d71b114e7a3 avoid proliferation of language_document reports;
wenzelm
parents: 67381
diff changeset
    26
      NONE => ignore (output_document state markdown txt)
67381
146757999c8d theory Pure is default presentation context;
wenzelm
parents: 64556
diff changeset
    27
    | SOME (_, pos) =>
146757999c8d theory Pure is default presentation context;
wenzelm
parents: 64556
diff changeset
    28
        error ("Illegal target specification -- not a theory context" ^ Position.here pos))) o
146757999c8d theory Pure is default presentation context;
wenzelm
parents: 64556
diff changeset
    29
  Toplevel.present_local_theory loc (fn state =>
67569
5d71b114e7a3 avoid proliferation of language_document reports;
wenzelm
parents: 67381
diff changeset
    30
    ignore (output_document state markdown txt));
67381
146757999c8d theory Pure is default presentation context;
wenzelm
parents: 64556
diff changeset
    31
58928
23d0ffd48006 plain value Keywords.keywords, which might be used outside theory for bootstrap purposes;
wenzelm
parents: 58918
diff changeset
    32
val _ =
64556
851ae0e7b09c more symbols;
wenzelm
parents: 62912
diff changeset
    33
  Outer_Syntax.command ("chapter", \<^here>) "chapter heading"
67381
146757999c8d theory Pure is default presentation context;
wenzelm
parents: 64556
diff changeset
    34
    (Parse.opt_target -- Parse.document_source --| semi >> 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
    35
ed09ae4ea2d8 uniform treatment of all document markup commands: 'text' and 'txt' merely differ in LaTeX style;
wenzelm
parents: 58928
diff changeset
    36
val _ =
64556
851ae0e7b09c more symbols;
wenzelm
parents: 62912
diff changeset
    37
  Outer_Syntax.command ("section", \<^here>) "section heading"
67381
146757999c8d theory Pure is default presentation context;
wenzelm
parents: 64556
diff changeset
    38
    (Parse.opt_target -- Parse.document_source --| semi >> document_command {markdown = false});
58918
8d36bc5eaed3 simplified keyword kinds;
wenzelm
parents: 58852
diff changeset
    39
48879
cb5cdbb645cd clarified bootstrapping of Pure;
wenzelm
parents:
diff changeset
    40
val _ =
64556
851ae0e7b09c more symbols;
wenzelm
parents: 62912
diff changeset
    41
  Outer_Syntax.command ("subsection", \<^here>) "subsection heading"
67381
146757999c8d theory Pure is default presentation context;
wenzelm
parents: 64556
diff changeset
    42
    (Parse.opt_target -- Parse.document_source --| semi >> 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
    43
ed09ae4ea2d8 uniform treatment of all document markup commands: 'text' and 'txt' merely differ in LaTeX style;
wenzelm
parents: 58928
diff changeset
    44
val _ =
64556
851ae0e7b09c more symbols;
wenzelm
parents: 62912
diff changeset
    45
  Outer_Syntax.command ("subsubsection", \<^here>) "subsubsection heading"
67381
146757999c8d theory Pure is default presentation context;
wenzelm
parents: 64556
diff changeset
    46
    (Parse.opt_target -- Parse.document_source --| semi >> document_command {markdown = false});
58928
23d0ffd48006 plain value Keywords.keywords, which might be used outside theory for bootstrap purposes;
wenzelm
parents: 58918
diff changeset
    47
23d0ffd48006 plain value Keywords.keywords, which might be used outside theory for bootstrap purposes;
wenzelm
parents: 58918
diff changeset
    48
val _ =
64556
851ae0e7b09c more symbols;
wenzelm
parents: 62912
diff changeset
    49
  Outer_Syntax.command ("paragraph", \<^here>) "paragraph heading"
67381
146757999c8d theory Pure is default presentation context;
wenzelm
parents: 64556
diff changeset
    50
    (Parse.opt_target -- Parse.document_source --| semi >> document_command {markdown = false});
61463
8e46cea6a45a added 'paragraph', 'subparagraph';
wenzelm
parents: 61457
diff changeset
    51
8e46cea6a45a added 'paragraph', 'subparagraph';
wenzelm
parents: 61457
diff changeset
    52
val _ =
64556
851ae0e7b09c more symbols;
wenzelm
parents: 62912
diff changeset
    53
  Outer_Syntax.command ("subparagraph", \<^here>) "subparagraph heading"
67381
146757999c8d theory Pure is default presentation context;
wenzelm
parents: 64556
diff changeset
    54
    (Parse.opt_target -- Parse.document_source --| semi >> document_command {markdown = false});
61463
8e46cea6a45a added 'paragraph', 'subparagraph';
wenzelm
parents: 61457
diff changeset
    55
8e46cea6a45a added 'paragraph', 'subparagraph';
wenzelm
parents: 61457
diff changeset
    56
val _ =
64556
851ae0e7b09c more symbols;
wenzelm
parents: 62912
diff changeset
    57
  Outer_Syntax.command ("text", \<^here>) "formal comment (primary style)"
67381
146757999c8d theory Pure is default presentation context;
wenzelm
parents: 64556
diff changeset
    58
    (Parse.opt_target -- Parse.document_source >> document_command {markdown = true});
58928
23d0ffd48006 plain value Keywords.keywords, which might be used outside theory for bootstrap purposes;
wenzelm
parents: 58918
diff changeset
    59
23d0ffd48006 plain value Keywords.keywords, which might be used outside theory for bootstrap purposes;
wenzelm
parents: 58918
diff changeset
    60
val _ =
64556
851ae0e7b09c more symbols;
wenzelm
parents: 62912
diff changeset
    61
  Outer_Syntax.command ("txt", \<^here>) "formal comment (secondary style)"
67381
146757999c8d theory Pure is default presentation context;
wenzelm
parents: 64556
diff changeset
    62
    (Parse.opt_target -- Parse.document_source >> 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
    63
ed09ae4ea2d8 uniform treatment of all document markup commands: 'text' and 'txt' merely differ in LaTeX style;
wenzelm
parents: 58928
diff changeset
    64
val _ =
64556
851ae0e7b09c more symbols;
wenzelm
parents: 62912
diff changeset
    65
  Outer_Syntax.command ("text_raw", \<^here>) "LaTeX text (without surrounding environment)"
67381
146757999c8d theory Pure is default presentation context;
wenzelm
parents: 64556
diff changeset
    66
    (Parse.opt_target -- Parse.document_source >> document_command {markdown = true});
58928
23d0ffd48006 plain value Keywords.keywords, which might be used outside theory for bootstrap purposes;
wenzelm
parents: 58918
diff changeset
    67
23d0ffd48006 plain value Keywords.keywords, which might be used outside theory for bootstrap purposes;
wenzelm
parents: 58918
diff changeset
    68
val _ =
64556
851ae0e7b09c more symbols;
wenzelm
parents: 62912
diff changeset
    69
  Outer_Syntax.command ("theory", \<^here>) "begin theory"
58852
621c052789b4 obsolete;
wenzelm
parents: 58842
diff changeset
    70
    (Thy_Header.args >>
621c052789b4 obsolete;
wenzelm
parents: 58842
diff changeset
    71
      (fn _ => Toplevel.init_theory (fn () => error "Missing theory initialization")));
48879
cb5cdbb645cd clarified bootstrapping of Pure;
wenzelm
parents:
diff changeset
    72
60095
35f626b11422 more explicit bootstrap_thy;
wenzelm
parents: 58999
diff changeset
    73
62876
507c90523113 clarified modules -- simplified bootstrap;
wenzelm
parents: 62453
diff changeset
    74
val bootstrap_thy = Context.the_global_context ();
60095
35f626b11422 more explicit bootstrap_thy;
wenzelm
parents: 58999
diff changeset
    75
35f626b11422 more explicit bootstrap_thy;
wenzelm
parents: 58999
diff changeset
    76
val _ = Theory.setup (Config.put_global Outer_Syntax.bootstrap false);
35f626b11422 more explicit bootstrap_thy;
wenzelm
parents: 58999
diff changeset
    77
48879
cb5cdbb645cd clarified bootstrapping of Pure;
wenzelm
parents:
diff changeset
    78
end;