src/Pure/Thy/document_antiquotations.ML
author wenzelm
Thu Nov 19 22:06:14 2015 +0100 (2015-11-19)
changeset 61705 546e6494049f
parent 61704 3a010273df63
child 61748 fc53fbf9fe01
permissions -rw-r--r--
trim lines for @{theory_text} similarly to @{text};
wenzelm@61619
     1
(*  Title:      Pure/ML/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@61619
    79
        in
wenzelm@61619
    80
          implode (map Latex.output_token toks) |>
wenzelm@61619
    81
           (if Config.get ctxt Thy_Output.display
wenzelm@61619
    82
            then Latex.environment "isabelle"
wenzelm@61619
    83
            else enclose "\\isa{" "}")
wenzelm@61619
    84
        end));
wenzelm@61619
    85
wenzelm@61619
    86
wenzelm@61619
    87
(* goal state *)
wenzelm@61619
    88
wenzelm@61619
    89
local
wenzelm@61619
    90
wenzelm@61619
    91
fun goal_state name main = Thy_Output.antiquotation name (Scan.succeed ())
wenzelm@61619
    92
  (fn {state, context = ctxt, ...} => fn () =>
wenzelm@61619
    93
    Thy_Output.output ctxt
wenzelm@61619
    94
      [Goal_Display.pretty_goal
wenzelm@61619
    95
        (Config.put Goal_Display.show_main_goal main ctxt)
wenzelm@61619
    96
        (#goal (Proof.goal (Toplevel.proof_of state)))]);
wenzelm@61619
    97
wenzelm@61619
    98
in
wenzelm@61619
    99
wenzelm@61619
   100
val _ = Theory.setup
wenzelm@61619
   101
 (goal_state @{binding goals} true #>
wenzelm@61619
   102
  goal_state @{binding subgoals} false);
wenzelm@61619
   103
wenzelm@61619
   104
end;
wenzelm@61619
   105
wenzelm@61619
   106
wenzelm@61619
   107
(* embedded lemma *)
wenzelm@61619
   108
wenzelm@61619
   109
val _ = Theory.setup
wenzelm@61619
   110
  (Thy_Output.antiquotation @{binding lemma}
wenzelm@61619
   111
    (Scan.lift (Scan.ahead Parse.not_eof) -- Args.prop --
wenzelm@61619
   112
      Scan.lift (Parse.position (Parse.reserved "by") -- Method.parse -- Scan.option Method.parse))
wenzelm@61619
   113
    (fn {source, context = ctxt, ...} => fn ((prop_token, prop), (((_, by_pos), m1), m2)) =>
wenzelm@61619
   114
      let
wenzelm@61619
   115
        val prop_src = Token.src (Token.name_of_src source) [prop_token];
wenzelm@61619
   116
wenzelm@61619
   117
        val reports = (by_pos, Markup.keyword1) :: maps Method.reports_of (m1 :: the_list m2);
wenzelm@61619
   118
        val _ = Context_Position.reports ctxt reports;
wenzelm@61619
   119
wenzelm@61619
   120
        (* FIXME check proof!? *)
wenzelm@61619
   121
        val _ = ctxt
wenzelm@61619
   122
          |> Proof.theorem NONE (K I) [[(prop, [])]]
wenzelm@61619
   123
          |> Proof.global_terminal_proof (m1, m2);
wenzelm@61619
   124
      in
wenzelm@61619
   125
        Thy_Output.output ctxt
wenzelm@61619
   126
          (Thy_Output.maybe_pretty_source Thy_Output.pretty_term ctxt prop_src [prop])
wenzelm@61619
   127
      end));
wenzelm@61619
   128
wenzelm@61619
   129
wenzelm@61619
   130
(* verbatim text *)
wenzelm@61619
   131
wenzelm@61619
   132
val _ =
wenzelm@61619
   133
  Theory.setup
wenzelm@61619
   134
    (Thy_Output.antiquotation @{binding verbatim} (Scan.lift Args.text)
wenzelm@61619
   135
      (Thy_Output.verbatim_text o #context));
wenzelm@61619
   136
wenzelm@61619
   137
wenzelm@61619
   138
(* ML text *)
wenzelm@61619
   139
wenzelm@61619
   140
local
wenzelm@61619
   141
wenzelm@61619
   142
fun ml_text name ml = Thy_Output.antiquotation name (Scan.lift Args.text_input)
wenzelm@61619
   143
  (fn {context = ctxt, ...} => fn source =>
wenzelm@61619
   144
   (ML_Context.eval_in (SOME ctxt) ML_Compiler.flags (Input.pos_of source) (ml source);
wenzelm@61619
   145
    Thy_Output.verbatim_text ctxt (Input.source_content source)));
wenzelm@61619
   146
wenzelm@61619
   147
fun ml_enclose bg en source =
wenzelm@61619
   148
  ML_Lex.read bg @ ML_Lex.read_source false source @ ML_Lex.read en;
wenzelm@61619
   149
wenzelm@61619
   150
in
wenzelm@61619
   151
wenzelm@61619
   152
val _ = Theory.setup
wenzelm@61619
   153
 (ml_text @{binding ML} (ml_enclose "fn _ => (" ");") #>
wenzelm@61619
   154
  ml_text @{binding ML_op} (ml_enclose "fn _ => (op " ");") #>
wenzelm@61619
   155
  ml_text @{binding ML_type} (ml_enclose "val _ = NONE : (" ") option;") #>
wenzelm@61619
   156
  ml_text @{binding ML_structure}
wenzelm@61619
   157
    (ml_enclose "functor XXX() = struct structure XX = " " end;") #>
wenzelm@61619
   158
wenzelm@61619
   159
  ml_text @{binding ML_functor}   (* FIXME formal treatment of functor name (!?) *)
wenzelm@61619
   160
    (fn source =>
wenzelm@61619
   161
      ML_Lex.read ("ML_Env.check_functor " ^
wenzelm@61619
   162
        ML_Syntax.print_string (Input.source_content source))) #>
wenzelm@61619
   163
wenzelm@61619
   164
  ml_text @{binding ML_text} (K []));
wenzelm@61619
   165
wenzelm@61619
   166
end;
wenzelm@61619
   167
wenzelm@61619
   168
wenzelm@61619
   169
(* URLs *)
wenzelm@61619
   170
wenzelm@61619
   171
val _ = Theory.setup
wenzelm@61619
   172
  (Thy_Output.antiquotation @{binding url} (Scan.lift (Parse.position Parse.name))
wenzelm@61619
   173
    (fn {context = ctxt, ...} => fn (name, pos) =>
wenzelm@61619
   174
      (Context_Position.reports ctxt [(pos, Markup.language_path), (pos, Markup.url name)];
wenzelm@61619
   175
       enclose "\\url{" "}" name)));
wenzelm@61619
   176
wenzelm@61623
   177
wenzelm@61660
   178
(* doc entries *)
wenzelm@61660
   179
wenzelm@61660
   180
val _ = Theory.setup
wenzelm@61660
   181
  (Thy_Output.antiquotation @{binding doc} (Scan.lift (Parse.position Parse.name))
wenzelm@61660
   182
    (fn {context = ctxt, ...} => fn (name, pos) =>
wenzelm@61660
   183
      (Context_Position.report ctxt pos (Markup.doc name);
wenzelm@61660
   184
        Thy_Output.output ctxt [Thy_Output.pretty_text ctxt name])));
wenzelm@61660
   185
wenzelm@61660
   186
wenzelm@61623
   187
(* formal entities *)
wenzelm@61623
   188
wenzelm@61623
   189
fun entity_antiquotation name check output =
wenzelm@61623
   190
  Thy_Output.antiquotation name (Scan.lift (Parse.position Args.name))
wenzelm@61623
   191
    (fn {context = ctxt, ...} => fn (name, pos) => (check ctxt (name, pos); output name));
wenzelm@61623
   192
wenzelm@61623
   193
val _ =
wenzelm@61623
   194
  Theory.setup
wenzelm@61623
   195
   (entity_antiquotation @{binding command} Outer_Syntax.check_command
wenzelm@61623
   196
     (enclose "\\isacommand{" "}" o Output.output) #>
wenzelm@61623
   197
    entity_antiquotation @{binding method} Method.check_name Output.output #>
wenzelm@61623
   198
    entity_antiquotation @{binding attribute} Attrib.check_name Output.output);
wenzelm@61623
   199
wenzelm@61619
   200
end;