src/Pure/Thy/document_antiquotations.ML
author wenzelm
Tue Jan 05 13:48:51 2016 +0100 (2016-01-05)
changeset 62058 1cfd5d604937
parent 61814 1ca1142e1711
child 62153 df566b87e269
permissions -rw-r--r--
updated headers;
wenzelm@62058
     1
(*  Title:      Pure/Thy/document_antiquotations.ML
wenzelm@61619
     2
    Author:     Makarius
wenzelm@61619
     3
wenzelm@61619
     4
Miscellaneous document antiquotations.
wenzelm@61619
     5
*)
wenzelm@61619
     6
wenzelm@61619
     7
structure Document_Antiquotations: sig end =
wenzelm@61619
     8
struct
wenzelm@61619
     9
wenzelm@61619
    10
(* control spacing *)
wenzelm@61619
    11
wenzelm@61619
    12
val _ =
wenzelm@61619
    13
  Theory.setup
wenzelm@61704
    14
   (Thy_Output.antiquotation @{binding noindent} (Scan.succeed ()) (K (K "\\noindent")) #>
wenzelm@61704
    15
    Thy_Output.antiquotation @{binding smallskip} (Scan.succeed ()) (K (K "\\smallskip")) #>
wenzelm@61704
    16
    Thy_Output.antiquotation @{binding medskip} (Scan.succeed ()) (K (K "\\medskip")) #>
wenzelm@61704
    17
    Thy_Output.antiquotation @{binding bigskip} (Scan.succeed ()) (K (K "\\bigskip")));
wenzelm@61619
    18
wenzelm@61619
    19
wenzelm@61619
    20
(* control style *)
wenzelm@61619
    21
wenzelm@61619
    22
local
wenzelm@61619
    23
wenzelm@61619
    24
fun control_antiquotation name s1 s2 =
wenzelm@61619
    25
  Thy_Output.antiquotation name (Scan.lift Args.cartouche_input)
wenzelm@61619
    26
    (fn {state, ...} => enclose s1 s2 o Thy_Output.output_text state {markdown = false});
wenzelm@61619
    27
wenzelm@61619
    28
in
wenzelm@61619
    29
wenzelm@61619
    30
val _ =
wenzelm@61619
    31
  Theory.setup
wenzelm@61619
    32
   (control_antiquotation @{binding footnote} "\\footnote{" "}" #>
wenzelm@61619
    33
    control_antiquotation @{binding emph} "\\emph{" "}" #>
wenzelm@61619
    34
    control_antiquotation @{binding bold} "\\textbf{" "}");
wenzelm@61619
    35
wenzelm@61619
    36
end;
wenzelm@61619
    37
wenzelm@61619
    38
wenzelm@61619
    39
(* quasi-formal text (unchecked) *)
wenzelm@61619
    40
wenzelm@61619
    41
local
wenzelm@61619
    42
wenzelm@61619
    43
fun text_antiquotation name =
wenzelm@61619
    44
  Thy_Output.antiquotation name (Scan.lift Args.text_input)
wenzelm@61619
    45
    (fn {context = ctxt, ...} => fn source =>
wenzelm@61619
    46
     (Context_Position.report ctxt (Input.pos_of source)
wenzelm@61619
    47
        (Markup.language_text (Input.is_delimited source));
wenzelm@61619
    48
      Thy_Output.output ctxt [Thy_Output.pretty_text ctxt (Input.source_content source)]));
wenzelm@61619
    49
wenzelm@61619
    50
in
wenzelm@61619
    51
wenzelm@61619
    52
val _ =
wenzelm@61619
    53
  Theory.setup
wenzelm@61619
    54
   (text_antiquotation @{binding text} #>
wenzelm@61619
    55
    text_antiquotation @{binding cartouche});
wenzelm@61619
    56
wenzelm@61619
    57
end;
wenzelm@61619
    58
wenzelm@61619
    59
wenzelm@61619
    60
(* theory text with tokens (unchecked) *)
wenzelm@61619
    61
wenzelm@61619
    62
val _ =
wenzelm@61619
    63
  Theory.setup
wenzelm@61619
    64
    (Thy_Output.antiquotation @{binding theory_text} (Scan.lift Args.text_input)
wenzelm@61619
    65
      (fn {context = ctxt, ...} => fn source =>
wenzelm@61619
    66
        let
wenzelm@61619
    67
          val _ =
wenzelm@61619
    68
            Context_Position.report ctxt (Input.pos_of source)
wenzelm@61619
    69
              (Markup.language_outer (Input.is_delimited source));
wenzelm@61619
    70
wenzelm@61619
    71
          val keywords = Thy_Header.get_keywords' ctxt;
wenzelm@61619
    72
          val toks =
wenzelm@61705
    73
            Input.source_explode source
wenzelm@61705
    74
            |> not (Config.get ctxt Thy_Output.display) ? Symbol_Pos.trim_lines
wenzelm@61705
    75
            |> Source.of_list
wenzelm@61619
    76
            |> Token.source' true keywords
wenzelm@61619
    77
            |> Source.exhaust;
wenzelm@61619
    78
          val _ = Context_Position.reports_text ctxt (maps (Token.reports keywords) toks);
wenzelm@61748
    79
          val indentation =
wenzelm@61748
    80
            Latex.output_symbols (replicate (Config.get ctxt Thy_Output.indent) Symbol.space);
wenzelm@61619
    81
        in
wenzelm@61619
    82
          implode (map Latex.output_token toks) |>
wenzelm@61748
    83
           (if Config.get ctxt Thy_Output.display then
wenzelm@61748
    84
              split_lines #> map (prefix indentation) #> cat_lines #>
wenzelm@61748
    85
              Latex.environment "isabelle"
wenzelm@61619
    86
            else enclose "\\isa{" "}")
wenzelm@61619
    87
        end));
wenzelm@61619
    88
wenzelm@61619
    89
wenzelm@61619
    90
(* goal state *)
wenzelm@61619
    91
wenzelm@61619
    92
local
wenzelm@61619
    93
wenzelm@61619
    94
fun goal_state name main = Thy_Output.antiquotation name (Scan.succeed ())
wenzelm@61619
    95
  (fn {state, context = ctxt, ...} => fn () =>
wenzelm@61619
    96
    Thy_Output.output ctxt
wenzelm@61619
    97
      [Goal_Display.pretty_goal
wenzelm@61619
    98
        (Config.put Goal_Display.show_main_goal main ctxt)
wenzelm@61619
    99
        (#goal (Proof.goal (Toplevel.proof_of state)))]);
wenzelm@61619
   100
wenzelm@61619
   101
in
wenzelm@61619
   102
wenzelm@61619
   103
val _ = Theory.setup
wenzelm@61619
   104
 (goal_state @{binding goals} true #>
wenzelm@61619
   105
  goal_state @{binding subgoals} false);
wenzelm@61619
   106
wenzelm@61619
   107
end;
wenzelm@61619
   108
wenzelm@61619
   109
wenzelm@61619
   110
(* embedded lemma *)
wenzelm@61619
   111
wenzelm@61619
   112
val _ = Theory.setup
wenzelm@61619
   113
  (Thy_Output.antiquotation @{binding lemma}
wenzelm@61619
   114
    (Scan.lift (Scan.ahead Parse.not_eof) -- Args.prop --
wenzelm@61619
   115
      Scan.lift (Parse.position (Parse.reserved "by") -- Method.parse -- Scan.option Method.parse))
wenzelm@61619
   116
    (fn {source, context = ctxt, ...} => fn ((prop_token, prop), (((_, by_pos), m1), m2)) =>
wenzelm@61619
   117
      let
wenzelm@61619
   118
        val reports = (by_pos, Markup.keyword1) :: maps Method.reports_of (m1 :: the_list m2);
wenzelm@61619
   119
        val _ = Context_Position.reports ctxt reports;
wenzelm@61619
   120
wenzelm@61619
   121
        (* FIXME check proof!? *)
wenzelm@61619
   122
        val _ = ctxt
wenzelm@61619
   123
          |> Proof.theorem NONE (K I) [[(prop, [])]]
wenzelm@61619
   124
          |> Proof.global_terminal_proof (m1, m2);
wenzelm@61619
   125
      in
wenzelm@61619
   126
        Thy_Output.output ctxt
wenzelm@61814
   127
          (Thy_Output.maybe_pretty_source
wenzelm@61814
   128
            Thy_Output.pretty_term ctxt [hd source, prop_token] [prop])
wenzelm@61619
   129
      end));
wenzelm@61619
   130
wenzelm@61619
   131
wenzelm@61619
   132
(* verbatim text *)
wenzelm@61619
   133
wenzelm@61619
   134
val _ =
wenzelm@61619
   135
  Theory.setup
wenzelm@61619
   136
    (Thy_Output.antiquotation @{binding verbatim} (Scan.lift Args.text)
wenzelm@61619
   137
      (Thy_Output.verbatim_text o #context));
wenzelm@61619
   138
wenzelm@61619
   139
wenzelm@61619
   140
(* ML text *)
wenzelm@61619
   141
wenzelm@61619
   142
local
wenzelm@61619
   143
wenzelm@61619
   144
fun ml_text name ml = Thy_Output.antiquotation name (Scan.lift Args.text_input)
wenzelm@61619
   145
  (fn {context = ctxt, ...} => fn source =>
wenzelm@61619
   146
   (ML_Context.eval_in (SOME ctxt) ML_Compiler.flags (Input.pos_of source) (ml source);
wenzelm@61619
   147
    Thy_Output.verbatim_text ctxt (Input.source_content source)));
wenzelm@61619
   148
wenzelm@61619
   149
fun ml_enclose bg en source =
wenzelm@61619
   150
  ML_Lex.read bg @ ML_Lex.read_source false source @ ML_Lex.read en;
wenzelm@61619
   151
wenzelm@61619
   152
in
wenzelm@61619
   153
wenzelm@61619
   154
val _ = Theory.setup
wenzelm@61619
   155
 (ml_text @{binding ML} (ml_enclose "fn _ => (" ");") #>
wenzelm@61619
   156
  ml_text @{binding ML_op} (ml_enclose "fn _ => (op " ");") #>
wenzelm@61619
   157
  ml_text @{binding ML_type} (ml_enclose "val _ = NONE : (" ") option;") #>
wenzelm@61619
   158
  ml_text @{binding ML_structure}
wenzelm@61619
   159
    (ml_enclose "functor XXX() = struct structure XX = " " end;") #>
wenzelm@61619
   160
wenzelm@61619
   161
  ml_text @{binding ML_functor}   (* FIXME formal treatment of functor name (!?) *)
wenzelm@61619
   162
    (fn source =>
wenzelm@61619
   163
      ML_Lex.read ("ML_Env.check_functor " ^
wenzelm@61619
   164
        ML_Syntax.print_string (Input.source_content source))) #>
wenzelm@61619
   165
wenzelm@61619
   166
  ml_text @{binding ML_text} (K []));
wenzelm@61619
   167
wenzelm@61619
   168
end;
wenzelm@61619
   169
wenzelm@61619
   170
wenzelm@61619
   171
(* URLs *)
wenzelm@61619
   172
wenzelm@61619
   173
val _ = Theory.setup
wenzelm@61619
   174
  (Thy_Output.antiquotation @{binding url} (Scan.lift (Parse.position Parse.name))
wenzelm@61619
   175
    (fn {context = ctxt, ...} => fn (name, pos) =>
wenzelm@61619
   176
      (Context_Position.reports ctxt [(pos, Markup.language_path), (pos, Markup.url name)];
wenzelm@61619
   177
       enclose "\\url{" "}" name)));
wenzelm@61619
   178
wenzelm@61623
   179
wenzelm@61660
   180
(* doc entries *)
wenzelm@61660
   181
wenzelm@61660
   182
val _ = Theory.setup
wenzelm@61660
   183
  (Thy_Output.antiquotation @{binding doc} (Scan.lift (Parse.position Parse.name))
wenzelm@61660
   184
    (fn {context = ctxt, ...} => fn (name, pos) =>
wenzelm@61660
   185
      (Context_Position.report ctxt pos (Markup.doc name);
wenzelm@61660
   186
        Thy_Output.output ctxt [Thy_Output.pretty_text ctxt name])));
wenzelm@61660
   187
wenzelm@61660
   188
wenzelm@61623
   189
(* formal entities *)
wenzelm@61623
   190
wenzelm@61623
   191
fun entity_antiquotation name check output =
wenzelm@61623
   192
  Thy_Output.antiquotation name (Scan.lift (Parse.position Args.name))
wenzelm@61623
   193
    (fn {context = ctxt, ...} => fn (name, pos) => (check ctxt (name, pos); output name));
wenzelm@61623
   194
wenzelm@61623
   195
val _ =
wenzelm@61623
   196
  Theory.setup
wenzelm@61623
   197
   (entity_antiquotation @{binding command} Outer_Syntax.check_command
wenzelm@61623
   198
     (enclose "\\isacommand{" "}" o Output.output) #>
wenzelm@61623
   199
    entity_antiquotation @{binding method} Method.check_name Output.output #>
wenzelm@61623
   200
    entity_antiquotation @{binding attribute} Attrib.check_name Output.output);
wenzelm@61623
   201
wenzelm@61619
   202
end;