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