src/Doc/antiquote_setup.ML
author wenzelm
Thu, 21 Sep 2017 12:47:16 +0200
changeset 66682 c4cbe609f6a8
parent 62829 4141c2a8458b
child 67386 998e01d6f8fd
permissions -rw-r--r--
avoid duplicate message for @{action} in particular (see also @{action} within Pure);
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
48985
5386df44a037 renamed doc-src to src/Doc;
wenzelm
parents: 48899
diff changeset
     1
(*  Title:      Doc/antiquote_setup.ML
21375
ae8a112b62d7 Auxiliary antiquotations for Isabelle manuals.
wenzelm
parents:
diff changeset
     2
    Author:     Makarius
ae8a112b62d7 Auxiliary antiquotations for Isabelle manuals.
wenzelm
parents:
diff changeset
     3
26742
5a86bc79431c misc cleanup;
wenzelm
parents: 26710
diff changeset
     4
Auxiliary antiquotations for the Isabelle manuals.
21375
ae8a112b62d7 Auxiliary antiquotations for Isabelle manuals.
wenzelm
parents:
diff changeset
     5
*)
ae8a112b62d7 Auxiliary antiquotations for Isabelle manuals.
wenzelm
parents:
diff changeset
     6
56059
2390391584c2 some document antiquotations for Isabelle/jEdit elements;
wenzelm
parents: 55997
diff changeset
     7
structure Antiquote_Setup: sig end =
26742
5a86bc79431c misc cleanup;
wenzelm
parents: 26710
diff changeset
     8
struct
21375
ae8a112b62d7 Auxiliary antiquotations for Isabelle manuals.
wenzelm
parents:
diff changeset
     9
26742
5a86bc79431c misc cleanup;
wenzelm
parents: 26710
diff changeset
    10
(* misc utils *)
5a86bc79431c misc cleanup;
wenzelm
parents: 26710
diff changeset
    11
29736
ec3fc818b82e clean_string/clean_name: proper treatment of \<dash>;
wenzelm
parents: 29726
diff changeset
    12
fun translate f = Symbol.explode #> map f #> implode;
ec3fc818b82e clean_string/clean_name: proper treatment of \<dash>;
wenzelm
parents: 29726
diff changeset
    13
ec3fc818b82e clean_string/clean_name: proper treatment of \<dash>;
wenzelm
parents: 29726
diff changeset
    14
val clean_string = translate
26853
52cb0e965041 clean_string: map "_" to "\\_" (best used with underscore.sty);
wenzelm
parents: 26843
diff changeset
    15
  (fn "_" => "\\_"
30120
aaa4667285c8 uniform treatment of ML indexing, using general \indexdef macro for formal Isabelle/Isar entities;
wenzelm
parents: 29736
diff changeset
    16
    | "#" => "\\#"
52408
fa2dc6c6c94f updated operations on proof terms;
wenzelm
parents: 50239
diff changeset
    17
    | "$" => "\\$"
fa2dc6c6c94f updated operations on proof terms;
wenzelm
parents: 50239
diff changeset
    18
    | "%" => "\\%"
26897
044619358d3a clean_string: cover <;
wenzelm
parents: 26894
diff changeset
    19
    | "<" => "$<$"
26768
844068d16ba0 clean_string: handle { };
wenzelm
parents: 26756
diff changeset
    20
    | ">" => "$>$"
844068d16ba0 clean_string: handle { };
wenzelm
parents: 26756
diff changeset
    21
    | "{" => "\\{"
30120
aaa4667285c8 uniform treatment of ML indexing, using general \indexdef macro for formal Isabelle/Isar entities;
wenzelm
parents: 29736
diff changeset
    22
    | "|" => "$\\mid$"
26768
844068d16ba0 clean_string: handle { };
wenzelm
parents: 26756
diff changeset
    23
    | "}" => "\\}"
42666
fee67c099d03 use existing \<hyphen>;
wenzelm
parents: 42361
diff changeset
    24
    | "\<hyphen>" => "-"
26768
844068d16ba0 clean_string: handle { };
wenzelm
parents: 26756
diff changeset
    25
    | c => c);
26751
2b97ea3130c2 added setup for Isar entities;
wenzelm
parents: 26742
diff changeset
    26
31546
d58d6acab331 eliminated escaped symbols;
wenzelm
parents: 31297
diff changeset
    27
fun clean_name "\<dots>" = "dots"
26897
044619358d3a clean_string: cover <;
wenzelm
parents: 26894
diff changeset
    28
  | clean_name ".." = "ddot"
044619358d3a clean_string: cover <;
wenzelm
parents: 26894
diff changeset
    29
  | clean_name "." = "dot"
26910
aa6357b39212 tuned clean_name (underscore);
wenzelm
parents: 26903
diff changeset
    30
  | clean_name "_" = "underscore"
26897
044619358d3a clean_string: cover <;
wenzelm
parents: 26894
diff changeset
    31
  | clean_name "{" = "braceleft"
044619358d3a clean_string: cover <;
wenzelm
parents: 26894
diff changeset
    32
  | clean_name "}" = "braceright"
42666
fee67c099d03 use existing \<hyphen>;
wenzelm
parents: 42361
diff changeset
    33
  | clean_name s = s |> translate (fn "_" => "-" | "\<hyphen>" => "-" | c => c);
26897
044619358d3a clean_string: cover <;
wenzelm
parents: 26894
diff changeset
    34
26742
5a86bc79431c misc cleanup;
wenzelm
parents: 26710
diff changeset
    35
5a86bc79431c misc cleanup;
wenzelm
parents: 26710
diff changeset
    36
(* ML text *)
5a86bc79431c misc cleanup;
wenzelm
parents: 26710
diff changeset
    37
5a86bc79431c misc cleanup;
wenzelm
parents: 26710
diff changeset
    38
local
5a86bc79431c misc cleanup;
wenzelm
parents: 26710
diff changeset
    39
59067
dd8ec9138112 tuned signature;
wenzelm
parents: 59066
diff changeset
    40
fun ml_val (toks1, []) = ML_Lex.read "fn _ => (" @ toks1 @ ML_Lex.read ");"
dd8ec9138112 tuned signature;
wenzelm
parents: 59066
diff changeset
    41
  | ml_val (toks1, toks2) =
dd8ec9138112 tuned signature;
wenzelm
parents: 59066
diff changeset
    42
      ML_Lex.read "fn _ => (" @ toks1 @ ML_Lex.read " : " @ toks2 @ ML_Lex.read ");";
21375
ae8a112b62d7 Auxiliary antiquotations for Isabelle manuals.
wenzelm
parents:
diff changeset
    43
59067
dd8ec9138112 tuned signature;
wenzelm
parents: 59066
diff changeset
    44
fun ml_op (toks1, []) = ML_Lex.read "fn _ => (op " @ toks1 @ ML_Lex.read ");"
dd8ec9138112 tuned signature;
wenzelm
parents: 59066
diff changeset
    45
  | ml_op (toks1, toks2) =
dd8ec9138112 tuned signature;
wenzelm
parents: 59066
diff changeset
    46
      ML_Lex.read "fn _ => (op " @ toks1 @ ML_Lex.read " : " @ toks2 @ ML_Lex.read ");";
46261
b03897da3c90 document antiquotations for ML infix operators;
wenzelm
parents: 45675
diff changeset
    47
59067
dd8ec9138112 tuned signature;
wenzelm
parents: 59066
diff changeset
    48
fun ml_type (toks1, []) = ML_Lex.read "val _ = NONE : (" @ toks1 @ ML_Lex.read ") option;"
55831
3a9386b32211 more markup for ML source;
wenzelm
parents: 55828
diff changeset
    49
  | ml_type (toks1, toks2) =
59067
dd8ec9138112 tuned signature;
wenzelm
parents: 59066
diff changeset
    50
      ML_Lex.read "val _ = [NONE : (" @ toks1 @ ML_Lex.read ") option, NONE : (" @
dd8ec9138112 tuned signature;
wenzelm
parents: 59066
diff changeset
    51
        toks2 @ ML_Lex.read ") option];";
22289
41ce4f5c97c9 added antiquotation for exceptions
haftmann
parents: 22094
diff changeset
    52
59067
dd8ec9138112 tuned signature;
wenzelm
parents: 59066
diff changeset
    53
fun ml_exception (toks1, []) = ML_Lex.read "fn _ => (" @ toks1 @ ML_Lex.read " : exn);"
55837
154855d9a564 clarified names of antiquotations and markup;
wenzelm
parents: 55831
diff changeset
    54
  | ml_exception (toks1, toks2) =
59067
dd8ec9138112 tuned signature;
wenzelm
parents: 59066
diff changeset
    55
      ML_Lex.read "fn _ => (" @ toks1 @ ML_Lex.read " : " @ toks2 @ ML_Lex.read " -> exn);";
22289
41ce4f5c97c9 added antiquotation for exceptions
haftmann
parents: 22094
diff changeset
    56
55831
3a9386b32211 more markup for ML source;
wenzelm
parents: 55828
diff changeset
    57
fun ml_structure (toks, _) =
59067
dd8ec9138112 tuned signature;
wenzelm
parents: 59066
diff changeset
    58
  ML_Lex.read "functor XXX() = struct structure XX = " @ toks @ ML_Lex.read " end;";
21375
ae8a112b62d7 Auxiliary antiquotations for Isabelle manuals.
wenzelm
parents:
diff changeset
    59
55831
3a9386b32211 more markup for ML source;
wenzelm
parents: 55828
diff changeset
    60
fun ml_functor (Antiquote.Text tok :: _, _) =
59067
dd8ec9138112 tuned signature;
wenzelm
parents: 59066
diff changeset
    61
      ML_Lex.read "ML_Env.check_functor " @
dd8ec9138112 tuned signature;
wenzelm
parents: 59066
diff changeset
    62
      ML_Lex.read (ML_Syntax.print_string (ML_Lex.content_of tok))
55831
3a9386b32211 more markup for ML source;
wenzelm
parents: 55828
diff changeset
    63
  | ml_functor _ = raise Fail "Bad ML functor specification";
21375
ae8a112b62d7 Auxiliary antiquotations for Isabelle manuals.
wenzelm
parents:
diff changeset
    64
59082
wenzelm
parents: 59067
diff changeset
    65
val is_name =
wenzelm
parents: 59067
diff changeset
    66
  ML_Lex.kind_of #> (fn kind => kind = ML_Lex.Ident orelse kind = ML_Lex.Long_Ident);
39869
c269f6bd0a1f more robust index_ML antiquotations: guess name from text (affects infixes and type constructors in particular);
wenzelm
parents: 39858
diff changeset
    67
c269f6bd0a1f more robust index_ML antiquotations: guess name from text (affects infixes and type constructors in particular);
wenzelm
parents: 39858
diff changeset
    68
fun ml_name txt =
c269f6bd0a1f more robust index_ML antiquotations: guess name from text (affects infixes and type constructors in particular);
wenzelm
parents: 39858
diff changeset
    69
  (case filter is_name (ML_Lex.tokenize txt) of
c269f6bd0a1f more robust index_ML antiquotations: guess name from text (affects infixes and type constructors in particular);
wenzelm
parents: 39858
diff changeset
    70
    toks as [_] => ML_Lex.flatten toks
c269f6bd0a1f more robust index_ML antiquotations: guess name from text (affects infixes and type constructors in particular);
wenzelm
parents: 39858
diff changeset
    71
  | _ => error ("Single ML name expected in input: " ^ quote txt));
c269f6bd0a1f more robust index_ML antiquotations: guess name from text (affects infixes and type constructors in particular);
wenzelm
parents: 39858
diff changeset
    72
55831
3a9386b32211 more markup for ML source;
wenzelm
parents: 55828
diff changeset
    73
fun prep_ml source =
59066
45ab32a542fe tuned signature;
wenzelm
parents: 59064
diff changeset
    74
  (Input.source_content source, ML_Lex.read_source false source);
55831
3a9386b32211 more markup for ML source;
wenzelm
parents: 55828
diff changeset
    75
37216
3165bc303f66 modernized some structure names, keeping a few legacy aliases;
wenzelm
parents: 37198
diff changeset
    76
fun index_ml name kind ml = Thy_Output.antiquotation name
59809
87641097d0f3 tuned signature;
wenzelm
parents: 59175
diff changeset
    77
  (Scan.lift (Args.text_input -- Scan.option (Args.colon |-- Args.text_input)))
55831
3a9386b32211 more markup for ML source;
wenzelm
parents: 55828
diff changeset
    78
  (fn {context = ctxt, ...} => fn (source1, opt_source2) =>
30394
c11a1e65a2ed moved @{ML_functor} and @{ML_text} to Pure;
wenzelm
parents: 30382
diff changeset
    79
    let
55831
3a9386b32211 more markup for ML source;
wenzelm
parents: 55828
diff changeset
    80
      val (txt1, toks1) = prep_ml source1;
3a9386b32211 more markup for ML source;
wenzelm
parents: 55828
diff changeset
    81
      val (txt2, toks2) =
3a9386b32211 more markup for ML source;
wenzelm
parents: 55828
diff changeset
    82
        (case opt_source2 of
3a9386b32211 more markup for ML source;
wenzelm
parents: 55828
diff changeset
    83
          SOME source => prep_ml source
3a9386b32211 more markup for ML source;
wenzelm
parents: 55828
diff changeset
    84
        | NONE => ("", []));
3a9386b32211 more markup for ML source;
wenzelm
parents: 55828
diff changeset
    85
30394
c11a1e65a2ed moved @{ML_functor} and @{ML_text} to Pure;
wenzelm
parents: 30382
diff changeset
    86
      val txt =
c11a1e65a2ed moved @{ML_functor} and @{ML_text} to Pure;
wenzelm
parents: 30382
diff changeset
    87
        if txt2 = "" then txt1
c11a1e65a2ed moved @{ML_functor} and @{ML_text} to Pure;
wenzelm
parents: 30382
diff changeset
    88
        else if kind = "type" then txt1 ^ " = " ^ txt2
c11a1e65a2ed moved @{ML_functor} and @{ML_text} to Pure;
wenzelm
parents: 30382
diff changeset
    89
        else if kind = "exception" then txt1 ^ " of " ^ txt2
50239
fb579401dc26 tuned signature;
wenzelm
parents: 50201
diff changeset
    90
        else if Symbol_Pos.is_identifier (Long_Name.base_name (ml_name txt1))
42290
b1f544c84040 discontinued special treatment of structure Lexicon;
wenzelm
parents: 40801
diff changeset
    91
        then txt1 ^ ": " ^ txt2
39858
5be7a57c3b4e more robust treatment of symbolic indentifiers (which may contain colons);
wenzelm
parents: 39829
diff changeset
    92
        else txt1 ^ " : " ^ txt2;
30394
c11a1e65a2ed moved @{ML_functor} and @{ML_text} to Pure;
wenzelm
parents: 30382
diff changeset
    93
      val txt' = if kind = "" then txt else kind ^ " " ^ txt;
55831
3a9386b32211 more markup for ML source;
wenzelm
parents: 55828
diff changeset
    94
59064
a8bcb5a446c8 more abstract type Input.source;
wenzelm
parents: 58978
diff changeset
    95
      val pos = Input.pos_of source1;
56275
600f432ab556 added command 'SML_file' for Standard ML without Isabelle/ML add-ons;
wenzelm
parents: 56208
diff changeset
    96
      val _ =
57477
c3b5cb53ea79 redundant error position, to ensure the message is attached somewhere, despite the distortion of positions due to glued tokens;
wenzelm
parents: 57334
diff changeset
    97
        ML_Context.eval_in (SOME ctxt) ML_Compiler.flags pos (ml (toks1, toks2))
c3b5cb53ea79 redundant error position, to ensure the message is attached somewhere, despite the distortion of positions due to glued tokens;
wenzelm
parents: 57334
diff changeset
    98
          handle ERROR msg => error (msg ^ Position.here pos);
30394
c11a1e65a2ed moved @{ML_functor} and @{ML_text} to Pure;
wenzelm
parents: 30382
diff changeset
    99
      val kind' = if kind = "" then "ML" else "ML " ^ kind;
c11a1e65a2ed moved @{ML_functor} and @{ML_text} to Pure;
wenzelm
parents: 30382
diff changeset
   100
    in
39869
c269f6bd0a1f more robust index_ML antiquotations: guess name from text (affects infixes and type constructors in particular);
wenzelm
parents: 39858
diff changeset
   101
      "\\indexdef{}{" ^ kind' ^ "}{" ^ clean_string (ml_name txt1) ^ "}" ^
58716
23a380cc45f4 official support for "tt" style variants, avoid fragile \verb in LaTeX;
wenzelm
parents: 58069
diff changeset
   102
      (Thy_Output.verbatim_text ctxt txt')
30394
c11a1e65a2ed moved @{ML_functor} and @{ML_text} to Pure;
wenzelm
parents: 30382
diff changeset
   103
    end);
26742
5a86bc79431c misc cleanup;
wenzelm
parents: 26710
diff changeset
   104
5a86bc79431c misc cleanup;
wenzelm
parents: 26710
diff changeset
   105
in
21375
ae8a112b62d7 Auxiliary antiquotations for Isabelle manuals.
wenzelm
parents:
diff changeset
   106
56059
2390391584c2 some document antiquotations for Isabelle/jEdit elements;
wenzelm
parents: 55997
diff changeset
   107
val _ =
2390391584c2 some document antiquotations for Isabelle/jEdit elements;
wenzelm
parents: 55997
diff changeset
   108
  Theory.setup
2390391584c2 some document antiquotations for Isabelle/jEdit elements;
wenzelm
parents: 55997
diff changeset
   109
   (index_ml @{binding index_ML} "" ml_val #>
2390391584c2 some document antiquotations for Isabelle/jEdit elements;
wenzelm
parents: 55997
diff changeset
   110
    index_ml @{binding index_ML_op} "infix" ml_op #>
2390391584c2 some document antiquotations for Isabelle/jEdit elements;
wenzelm
parents: 55997
diff changeset
   111
    index_ml @{binding index_ML_type} "type" ml_type #>
2390391584c2 some document antiquotations for Isabelle/jEdit elements;
wenzelm
parents: 55997
diff changeset
   112
    index_ml @{binding index_ML_exception} "exception" ml_exception #>
2390391584c2 some document antiquotations for Isabelle/jEdit elements;
wenzelm
parents: 55997
diff changeset
   113
    index_ml @{binding index_ML_structure} "structure" ml_structure #>
2390391584c2 some document antiquotations for Isabelle/jEdit elements;
wenzelm
parents: 55997
diff changeset
   114
    index_ml @{binding index_ML_functor} "functor" ml_functor);
21375
ae8a112b62d7 Auxiliary antiquotations for Isabelle manuals.
wenzelm
parents:
diff changeset
   115
26742
5a86bc79431c misc cleanup;
wenzelm
parents: 26710
diff changeset
   116
end;
21375
ae8a112b62d7 Auxiliary antiquotations for Isabelle manuals.
wenzelm
parents:
diff changeset
   117
23846
bfedd1a024fc Added named_thms antiquotation.
berghofe
parents: 23651
diff changeset
   118
30394
c11a1e65a2ed moved @{ML_functor} and @{ML_text} to Pure;
wenzelm
parents: 30382
diff changeset
   119
(* named theorems *)
23846
bfedd1a024fc Added named_thms antiquotation.
berghofe
parents: 23651
diff changeset
   120
56059
2390391584c2 some document antiquotations for Isabelle/jEdit elements;
wenzelm
parents: 55997
diff changeset
   121
val _ =
2390391584c2 some document antiquotations for Isabelle/jEdit elements;
wenzelm
parents: 55997
diff changeset
   122
  Theory.setup (Thy_Output.antiquotation @{binding named_thms}
43564
9864182c6bad document antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents: 43563
diff changeset
   123
    (Scan.repeat (Attrib.thm -- Scan.lift (Args.parens Args.name)))
9864182c6bad document antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents: 43563
diff changeset
   124
    (fn {context = ctxt, ...} =>
9864182c6bad document antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents: 43563
diff changeset
   125
      map (apfst (Thy_Output.pretty_thm ctxt))
9864182c6bad document antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents: 43563
diff changeset
   126
      #> (if Config.get ctxt Thy_Output.quotes then map (apfst Pretty.quote) else I)
9864182c6bad document antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents: 43563
diff changeset
   127
      #> (if Config.get ctxt Thy_Output.display
9864182c6bad document antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents: 43563
diff changeset
   128
          then
9864182c6bad document antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents: 43563
diff changeset
   129
            map (fn (p, name) =>
59175
bf465f335e85 system option "pretty_margin" is superseded by "thy_output_margin";
wenzelm
parents: 59083
diff changeset
   130
              Output.output
bf465f335e85 system option "pretty_margin" is superseded by "thy_output_margin";
wenzelm
parents: 59083
diff changeset
   131
                (Thy_Output.string_of_margin ctxt
bf465f335e85 system option "pretty_margin" is superseded by "thy_output_margin";
wenzelm
parents: 59083
diff changeset
   132
                  (Pretty.indent (Config.get ctxt Thy_Output.indent) p)) ^
61877
276ad4354069 renamed Pretty.str_of to Pretty.unformatted_string_of to emphasize its meaning;
wenzelm
parents: 61621
diff changeset
   133
              "\\rulename{" ^
276ad4354069 renamed Pretty.str_of to Pretty.unformatted_string_of to emphasize its meaning;
wenzelm
parents: 61621
diff changeset
   134
              Output.output (Pretty.unformatted_string_of (Thy_Output.pretty_text ctxt name)) ^ "}")
43564
9864182c6bad document antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents: 43563
diff changeset
   135
            #> space_implode "\\par\\smallskip%\n"
61462
e16649b70107 clarified Latex.environment;
wenzelm
parents: 59809
diff changeset
   136
            #> Latex.environment "isabelle"
43564
9864182c6bad document antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents: 43563
diff changeset
   137
          else
9864182c6bad document antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents: 43563
diff changeset
   138
            map (fn (p, name) =>
61877
276ad4354069 renamed Pretty.str_of to Pretty.unformatted_string_of to emphasize its meaning;
wenzelm
parents: 61621
diff changeset
   139
              Output.output (Pretty.unformatted_string_of p) ^
276ad4354069 renamed Pretty.str_of to Pretty.unformatted_string_of to emphasize its meaning;
wenzelm
parents: 61621
diff changeset
   140
              "\\rulename{" ^
276ad4354069 renamed Pretty.str_of to Pretty.unformatted_string_of to emphasize its meaning;
wenzelm
parents: 61621
diff changeset
   141
              Output.output (Pretty.unformatted_string_of (Thy_Output.pretty_text ctxt name)) ^ "}")
43564
9864182c6bad document antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents: 43563
diff changeset
   142
            #> space_implode "\\par\\smallskip%\n"
56059
2390391584c2 some document antiquotations for Isabelle/jEdit elements;
wenzelm
parents: 55997
diff changeset
   143
            #> enclose "\\isa{" "}")));
26742
5a86bc79431c misc cleanup;
wenzelm
parents: 26710
diff changeset
   144
5a86bc79431c misc cleanup;
wenzelm
parents: 26710
diff changeset
   145
30394
c11a1e65a2ed moved @{ML_functor} and @{ML_text} to Pure;
wenzelm
parents: 30382
diff changeset
   146
(* Isabelle/Isar entities (with index) *)
26751
2b97ea3130c2 added setup for Isar entities;
wenzelm
parents: 26742
diff changeset
   147
2b97ea3130c2 added setup for Isar entities;
wenzelm
parents: 26742
diff changeset
   148
local
2b97ea3130c2 added setup for Isar entities;
wenzelm
parents: 26742
diff changeset
   149
61620
01db1bed4487 tuned signature;
wenzelm
parents: 61618
diff changeset
   150
fun no_check (_: Proof.context) (name, _: Position.T) = name;
26894
1120f6cc10b0 proper checking of various Isar elements;
wenzelm
parents: 26853
diff changeset
   151
61620
01db1bed4487 tuned signature;
wenzelm
parents: 61618
diff changeset
   152
fun check_keyword ctxt (name, pos) =
01db1bed4487 tuned signature;
wenzelm
parents: 61618
diff changeset
   153
  if Keyword.is_keyword (Thy_Header.get_keywords' ctxt) name then name
01db1bed4487 tuned signature;
wenzelm
parents: 61618
diff changeset
   154
  else error ("Bad outer syntax keyword " ^ quote name ^ Position.here pos);
53061
417cb0f713e0 more markup;
wenzelm
parents: 53045
diff changeset
   155
56467
8d7d6f17c6a7 more uniform ML/document antiquotations;
wenzelm
parents: 56304
diff changeset
   156
fun check_system_option ctxt (name, pos) =
8d7d6f17c6a7 more uniform ML/document antiquotations;
wenzelm
parents: 56304
diff changeset
   157
  (Context_Position.report ctxt pos (Options.default_markup (name, pos)); true)
8d7d6f17c6a7 more uniform ML/document antiquotations;
wenzelm
parents: 56304
diff changeset
   158
    handle ERROR _ => false;
8d7d6f17c6a7 more uniform ML/document antiquotations;
wenzelm
parents: 56304
diff changeset
   159
26751
2b97ea3130c2 added setup for Isar entities;
wenzelm
parents: 26742
diff changeset
   160
val arg = enclose "{" "}" o clean_string;
2b97ea3130c2 added setup for Isar entities;
wenzelm
parents: 26742
diff changeset
   161
56185
851c7b05eb92 more antiquotations;
wenzelm
parents: 56135
diff changeset
   162
fun entity check markup binding index =
37216
3165bc303f66 modernized some structure names, keeping a few legacy aliases;
wenzelm
parents: 37198
diff changeset
   163
  Thy_Output.antiquotation
56185
851c7b05eb92 more antiquotations;
wenzelm
parents: 56135
diff changeset
   164
    (binding |> Binding.map_name (fn name => name ^
43564
9864182c6bad document antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents: 43563
diff changeset
   165
      (case index of NONE => "" | SOME true => "_def" | SOME false => "_ref")))
53044
be27b6be8027 more markup via Name_Space.check;
wenzelm
parents: 52408
diff changeset
   166
    (Scan.lift (Scan.optional (Args.parens Args.name) "" -- Parse.position Args.name))
be27b6be8027 more markup via Name_Space.check;
wenzelm
parents: 52408
diff changeset
   167
    (fn {context = ctxt, ...} => fn (logic, (name, pos)) =>
30394
c11a1e65a2ed moved @{ML_functor} and @{ML_text} to Pure;
wenzelm
parents: 30382
diff changeset
   168
      let
56185
851c7b05eb92 more antiquotations;
wenzelm
parents: 56135
diff changeset
   169
        val kind = translate (fn "_" => " " | c => c) (Binding.name_of binding);
30394
c11a1e65a2ed moved @{ML_functor} and @{ML_text} to Pure;
wenzelm
parents: 30382
diff changeset
   170
        val hyper_name =
c11a1e65a2ed moved @{ML_functor} and @{ML_text} to Pure;
wenzelm
parents: 30382
diff changeset
   171
          "{" ^ Long_Name.append kind (Long_Name.append logic (clean_name name)) ^ "}";
c11a1e65a2ed moved @{ML_functor} and @{ML_text} to Pure;
wenzelm
parents: 30382
diff changeset
   172
        val hyper =
c11a1e65a2ed moved @{ML_functor} and @{ML_text} to Pure;
wenzelm
parents: 30382
diff changeset
   173
          enclose ("\\hyperlink" ^ hyper_name ^ "{") "}" #>
c11a1e65a2ed moved @{ML_functor} and @{ML_text} to Pure;
wenzelm
parents: 30382
diff changeset
   174
          index = SOME true ? enclose ("\\hypertarget" ^ hyper_name ^ "{") "}";
c11a1e65a2ed moved @{ML_functor} and @{ML_text} to Pure;
wenzelm
parents: 30382
diff changeset
   175
        val idx =
c11a1e65a2ed moved @{ML_functor} and @{ML_text} to Pure;
wenzelm
parents: 30382
diff changeset
   176
          (case index of
c11a1e65a2ed moved @{ML_functor} and @{ML_text} to Pure;
wenzelm
parents: 30382
diff changeset
   177
            NONE => ""
c11a1e65a2ed moved @{ML_functor} and @{ML_text} to Pure;
wenzelm
parents: 30382
diff changeset
   178
          | SOME is_def =>
c11a1e65a2ed moved @{ML_functor} and @{ML_text} to Pure;
wenzelm
parents: 30382
diff changeset
   179
              "\\index" ^ (if is_def then "def" else "ref") ^ arg logic ^ arg kind ^ arg name);
66682
c4cbe609f6a8 avoid duplicate message for @{action} in particular (see also @{action} within Pure);
wenzelm
parents: 62829
diff changeset
   180
        val _ =
c4cbe609f6a8 avoid duplicate message for @{action} in particular (see also @{action} within Pure);
wenzelm
parents: 62829
diff changeset
   181
          if Context_Position.is_reported ctxt pos then ignore (check ctxt (name, pos)) else ();
30394
c11a1e65a2ed moved @{ML_functor} and @{ML_text} to Pure;
wenzelm
parents: 30382
diff changeset
   182
      in
61620
01db1bed4487 tuned signature;
wenzelm
parents: 61618
diff changeset
   183
        idx ^
01db1bed4487 tuned signature;
wenzelm
parents: 61618
diff changeset
   184
        (Output.output name
01db1bed4487 tuned signature;
wenzelm
parents: 61618
diff changeset
   185
          |> (if markup = "" then I else enclose ("\\" ^ markup ^ "{") "}")
01db1bed4487 tuned signature;
wenzelm
parents: 61618
diff changeset
   186
          |> hyper o enclose "\\mbox{\\isa{" "}}")
30394
c11a1e65a2ed moved @{ML_functor} and @{ML_text} to Pure;
wenzelm
parents: 30382
diff changeset
   187
      end);
26897
044619358d3a clean_string: cover <;
wenzelm
parents: 26894
diff changeset
   188
26894
1120f6cc10b0 proper checking of various Isar elements;
wenzelm
parents: 26853
diff changeset
   189
fun entity_antiqs check markup kind =
43564
9864182c6bad document antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents: 43563
diff changeset
   190
  entity check markup kind NONE #>
9864182c6bad document antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents: 43563
diff changeset
   191
  entity check markup kind (SOME true) #>
9864182c6bad document antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents: 43563
diff changeset
   192
  entity check markup kind (SOME false);
26751
2b97ea3130c2 added setup for Isar entities;
wenzelm
parents: 26742
diff changeset
   193
2b97ea3130c2 added setup for Isar entities;
wenzelm
parents: 26742
diff changeset
   194
in
2b97ea3130c2 added setup for Isar entities;
wenzelm
parents: 26742
diff changeset
   195
56059
2390391584c2 some document antiquotations for Isabelle/jEdit elements;
wenzelm
parents: 55997
diff changeset
   196
val _ =
2390391584c2 some document antiquotations for Isabelle/jEdit elements;
wenzelm
parents: 55997
diff changeset
   197
  Theory.setup
56185
851c7b05eb92 more antiquotations;
wenzelm
parents: 56135
diff changeset
   198
   (entity_antiqs no_check "" @{binding syntax} #>
61620
01db1bed4487 tuned signature;
wenzelm
parents: 61618
diff changeset
   199
    entity_antiqs Outer_Syntax.check_command "isacommand" @{binding command} #>
01db1bed4487 tuned signature;
wenzelm
parents: 61618
diff changeset
   200
    entity_antiqs check_keyword "isakeyword" @{binding keyword} #>
01db1bed4487 tuned signature;
wenzelm
parents: 61618
diff changeset
   201
    entity_antiqs check_keyword "isakeyword" @{binding element} #>
01db1bed4487 tuned signature;
wenzelm
parents: 61618
diff changeset
   202
    entity_antiqs Method.check_name "" @{binding method} #>
01db1bed4487 tuned signature;
wenzelm
parents: 61618
diff changeset
   203
    entity_antiqs Attrib.check_name "" @{binding attribute} #>
56185
851c7b05eb92 more antiquotations;
wenzelm
parents: 56135
diff changeset
   204
    entity_antiqs no_check "" @{binding fact} #>
851c7b05eb92 more antiquotations;
wenzelm
parents: 56135
diff changeset
   205
    entity_antiqs no_check "" @{binding variable} #>
851c7b05eb92 more antiquotations;
wenzelm
parents: 56135
diff changeset
   206
    entity_antiqs no_check "" @{binding case} #>
61620
01db1bed4487 tuned signature;
wenzelm
parents: 61618
diff changeset
   207
    entity_antiqs Thy_Output.check_command "" @{binding antiquotation} #>
01db1bed4487 tuned signature;
wenzelm
parents: 61618
diff changeset
   208
    entity_antiqs Thy_Output.check_option "" @{binding antiquotation_option} #>
58716
23a380cc45f4 official support for "tt" style variants, avoid fragile \verb in LaTeX;
wenzelm
parents: 58069
diff changeset
   209
    entity_antiqs no_check "isasystem" @{binding setting} #>
23a380cc45f4 official support for "tt" style variants, avoid fragile \verb in LaTeX;
wenzelm
parents: 58069
diff changeset
   210
    entity_antiqs check_system_option "isasystem" @{binding system_option} #>
56185
851c7b05eb92 more antiquotations;
wenzelm
parents: 56135
diff changeset
   211
    entity_antiqs no_check "" @{binding inference} #>
58716
23a380cc45f4 official support for "tt" style variants, avoid fragile \verb in LaTeX;
wenzelm
parents: 58069
diff changeset
   212
    entity_antiqs no_check "isasystem" @{binding executable} #>
62829
4141c2a8458b clarified Isabelle tool wrapper: bash, Scala, no perl, no ML;
wenzelm
parents: 61877
diff changeset
   213
    entity_antiqs no_check "isatool" @{binding tool} #>
61620
01db1bed4487 tuned signature;
wenzelm
parents: 61618
diff changeset
   214
    entity_antiqs ML_Context.check_antiquotation "" @{binding ML_antiquotation} #>
61621
70b8085f51b4 more thorough check_action, including completion;
wenzelm
parents: 61620
diff changeset
   215
    entity_antiqs (K JEdit.check_action) "isasystem" @{binding action});
26751
2b97ea3130c2 added setup for Isar entities;
wenzelm
parents: 26742
diff changeset
   216
26742
5a86bc79431c misc cleanup;
wenzelm
parents: 26710
diff changeset
   217
end;
26751
2b97ea3130c2 added setup for Isar entities;
wenzelm
parents: 26742
diff changeset
   218
2b97ea3130c2 added setup for Isar entities;
wenzelm
parents: 26742
diff changeset
   219
end;