src/Pure/Thy/document_antiquotation.ML
author wenzelm
Sun, 26 Jul 2020 21:53:29 +0200
changeset 72305 9c0b835d4cc2
parent 70308 a0b21b4b7a4a
permissions -rw-r--r--
proper pretty printing for latex output, notably for pide_session=true (default);
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
67386
998e01d6f8fd clarified modules;
wenzelm
parents:
diff changeset
     1
(*  Title:      Pure/Thy/document_antiquotation.ML
998e01d6f8fd clarified modules;
wenzelm
parents:
diff changeset
     2
    Author:     Makarius
998e01d6f8fd clarified modules;
wenzelm
parents:
diff changeset
     3
998e01d6f8fd clarified modules;
wenzelm
parents:
diff changeset
     4
Document antiquotations.
998e01d6f8fd clarified modules;
wenzelm
parents:
diff changeset
     5
*)
998e01d6f8fd clarified modules;
wenzelm
parents:
diff changeset
     6
998e01d6f8fd clarified modules;
wenzelm
parents:
diff changeset
     7
signature DOCUMENT_ANTIQUOTATION =
998e01d6f8fd clarified modules;
wenzelm
parents:
diff changeset
     8
sig
998e01d6f8fd clarified modules;
wenzelm
parents:
diff changeset
     9
  val thy_output_display: bool Config.T
70307
61e26527480e added document antiquotation option "cartouche";
wenzelm
parents: 69604
diff changeset
    10
  val thy_output_cartouche: bool Config.T
67386
998e01d6f8fd clarified modules;
wenzelm
parents:
diff changeset
    11
  val thy_output_quotes: bool Config.T
998e01d6f8fd clarified modules;
wenzelm
parents:
diff changeset
    12
  val thy_output_margin: int Config.T
998e01d6f8fd clarified modules;
wenzelm
parents:
diff changeset
    13
  val thy_output_indent: int Config.T
998e01d6f8fd clarified modules;
wenzelm
parents:
diff changeset
    14
  val thy_output_source: bool Config.T
70308
a0b21b4b7a4a strip cartouches from arguments of "embedded" document antiquotations, corresponding to automated update via "isabelle update -u control_cartouches" -- e.g. relevant for documents with thy_output_source (e.g. doc "isar-ref", "jedit", "system");
wenzelm
parents: 70307
diff changeset
    15
  val thy_output_source_cartouche: bool Config.T
67386
998e01d6f8fd clarified modules;
wenzelm
parents:
diff changeset
    16
  val thy_output_break: bool Config.T
998e01d6f8fd clarified modules;
wenzelm
parents:
diff changeset
    17
  val thy_output_modes: string Config.T
67464
a5ca98950a91 clarified access to antiquotation options;
wenzelm
parents: 67461
diff changeset
    18
  val trim_blanks: Proof.context -> string -> string
a5ca98950a91 clarified access to antiquotation options;
wenzelm
parents: 67461
diff changeset
    19
  val trim_lines: Proof.context -> string -> string
a5ca98950a91 clarified access to antiquotation options;
wenzelm
parents: 67461
diff changeset
    20
  val indent_lines: Proof.context -> string -> string
67475
90def2b06305 more uniform output of source / text / theory_text, with handling of formal comments etc.;
wenzelm
parents: 67473
diff changeset
    21
  val prepare_lines: Proof.context -> string -> string
70307
61e26527480e added document antiquotation option "cartouche";
wenzelm
parents: 69604
diff changeset
    22
  val delimit: Proof.context -> Pretty.T -> Pretty.T
67464
a5ca98950a91 clarified access to antiquotation options;
wenzelm
parents: 67461
diff changeset
    23
  val indent: Proof.context -> Pretty.T -> Pretty.T
a5ca98950a91 clarified access to antiquotation options;
wenzelm
parents: 67461
diff changeset
    24
  val format: Proof.context -> Pretty.T -> string
a5ca98950a91 clarified access to antiquotation options;
wenzelm
parents: 67461
diff changeset
    25
  val output: Proof.context -> Pretty.T -> Output.output
67386
998e01d6f8fd clarified modules;
wenzelm
parents:
diff changeset
    26
  val print_antiquotations: bool -> Proof.context -> unit
998e01d6f8fd clarified modules;
wenzelm
parents:
diff changeset
    27
  val check: Proof.context -> xstring * Position.T -> string
998e01d6f8fd clarified modules;
wenzelm
parents:
diff changeset
    28
  val check_option: Proof.context -> xstring * Position.T -> string
998e01d6f8fd clarified modules;
wenzelm
parents:
diff changeset
    29
  val setup: binding -> 'a context_parser ->
67464
a5ca98950a91 clarified access to antiquotation options;
wenzelm
parents: 67461
diff changeset
    30
    ({context: Proof.context, source: Token.src, argument: 'a} -> Latex.text) -> theory -> theory
69604
a80d8ec6c998 support for isabelle update -u control_cartouches;
wenzelm
parents: 69359
diff changeset
    31
  val setup_embedded: binding -> 'a context_parser ->
a80d8ec6c998 support for isabelle update -u control_cartouches;
wenzelm
parents: 69359
diff changeset
    32
    ({context: Proof.context, source: Token.src, argument: 'a} -> Latex.text) -> theory -> theory
67386
998e01d6f8fd clarified modules;
wenzelm
parents:
diff changeset
    33
  val setup_option: binding -> (string -> Proof.context -> Proof.context) -> theory -> theory
998e01d6f8fd clarified modules;
wenzelm
parents:
diff changeset
    34
  val boolean: string -> bool
998e01d6f8fd clarified modules;
wenzelm
parents:
diff changeset
    35
  val integer: string -> int
67571
f858fe5531ac more uniform treatment of formal comments within document source;
wenzelm
parents: 67475
diff changeset
    36
  val evaluate: (Symbol_Pos.T list -> Latex.text list) -> Proof.context ->
f858fe5531ac more uniform treatment of formal comments within document source;
wenzelm
parents: 67475
diff changeset
    37
    Antiquote.text_antiquote -> Latex.text list
67386
998e01d6f8fd clarified modules;
wenzelm
parents:
diff changeset
    38
end;
998e01d6f8fd clarified modules;
wenzelm
parents:
diff changeset
    39
998e01d6f8fd clarified modules;
wenzelm
parents:
diff changeset
    40
structure Document_Antiquotation: DOCUMENT_ANTIQUOTATION =
998e01d6f8fd clarified modules;
wenzelm
parents:
diff changeset
    41
struct
998e01d6f8fd clarified modules;
wenzelm
parents:
diff changeset
    42
998e01d6f8fd clarified modules;
wenzelm
parents:
diff changeset
    43
(* options *)
998e01d6f8fd clarified modules;
wenzelm
parents:
diff changeset
    44
998e01d6f8fd clarified modules;
wenzelm
parents:
diff changeset
    45
val thy_output_display = Attrib.setup_option_bool ("thy_output_display", \<^here>);
998e01d6f8fd clarified modules;
wenzelm
parents:
diff changeset
    46
val thy_output_break = Attrib.setup_option_bool ("thy_output_break", \<^here>);
70307
61e26527480e added document antiquotation option "cartouche";
wenzelm
parents: 69604
diff changeset
    47
val thy_output_cartouche = Attrib.setup_option_bool ("thy_output_cartouche", \<^here>);
67386
998e01d6f8fd clarified modules;
wenzelm
parents:
diff changeset
    48
val thy_output_quotes = Attrib.setup_option_bool ("thy_output_quotes", \<^here>);
998e01d6f8fd clarified modules;
wenzelm
parents:
diff changeset
    49
val thy_output_margin = Attrib.setup_option_int ("thy_output_margin", \<^here>);
998e01d6f8fd clarified modules;
wenzelm
parents:
diff changeset
    50
val thy_output_indent = Attrib.setup_option_int ("thy_output_indent", \<^here>);
998e01d6f8fd clarified modules;
wenzelm
parents:
diff changeset
    51
val thy_output_source = Attrib.setup_option_bool ("thy_output_source", \<^here>);
70308
a0b21b4b7a4a strip cartouches from arguments of "embedded" document antiquotations, corresponding to automated update via "isabelle update -u control_cartouches" -- e.g. relevant for documents with thy_output_source (e.g. doc "isar-ref", "jedit", "system");
wenzelm
parents: 70307
diff changeset
    52
val thy_output_source_cartouche = Attrib.setup_option_bool ("thy_output_source_cartouche", \<^here>);
67386
998e01d6f8fd clarified modules;
wenzelm
parents:
diff changeset
    53
val thy_output_modes = Attrib.setup_option_string ("thy_output_modes", \<^here>);
998e01d6f8fd clarified modules;
wenzelm
parents:
diff changeset
    54
998e01d6f8fd clarified modules;
wenzelm
parents:
diff changeset
    55
67464
a5ca98950a91 clarified access to antiquotation options;
wenzelm
parents: 67461
diff changeset
    56
(* blanks *)
a5ca98950a91 clarified access to antiquotation options;
wenzelm
parents: 67461
diff changeset
    57
a5ca98950a91 clarified access to antiquotation options;
wenzelm
parents: 67461
diff changeset
    58
fun trim_blanks ctxt =
a5ca98950a91 clarified access to antiquotation options;
wenzelm
parents: 67461
diff changeset
    59
  not (Config.get ctxt thy_output_display) ? Symbol.trim_blanks;
a5ca98950a91 clarified access to antiquotation options;
wenzelm
parents: 67461
diff changeset
    60
a5ca98950a91 clarified access to antiquotation options;
wenzelm
parents: 67461
diff changeset
    61
fun trim_lines ctxt =
a5ca98950a91 clarified access to antiquotation options;
wenzelm
parents: 67461
diff changeset
    62
  if not (Config.get ctxt thy_output_display) then
a5ca98950a91 clarified access to antiquotation options;
wenzelm
parents: 67461
diff changeset
    63
    split_lines #> map Symbol.trim_blanks #> space_implode " "
a5ca98950a91 clarified access to antiquotation options;
wenzelm
parents: 67461
diff changeset
    64
  else I;
a5ca98950a91 clarified access to antiquotation options;
wenzelm
parents: 67461
diff changeset
    65
a5ca98950a91 clarified access to antiquotation options;
wenzelm
parents: 67461
diff changeset
    66
fun indent_lines ctxt =
a5ca98950a91 clarified access to antiquotation options;
wenzelm
parents: 67461
diff changeset
    67
  if Config.get ctxt thy_output_display then
a5ca98950a91 clarified access to antiquotation options;
wenzelm
parents: 67461
diff changeset
    68
    prefix_lines (Symbol.spaces (Config.get ctxt thy_output_indent))
a5ca98950a91 clarified access to antiquotation options;
wenzelm
parents: 67461
diff changeset
    69
  else I;
a5ca98950a91 clarified access to antiquotation options;
wenzelm
parents: 67461
diff changeset
    70
67475
90def2b06305 more uniform output of source / text / theory_text, with handling of formal comments etc.;
wenzelm
parents: 67473
diff changeset
    71
fun prepare_lines ctxt = trim_lines ctxt #> indent_lines ctxt;
90def2b06305 more uniform output of source / text / theory_text, with handling of formal comments etc.;
wenzelm
parents: 67473
diff changeset
    72
67464
a5ca98950a91 clarified access to antiquotation options;
wenzelm
parents: 67461
diff changeset
    73
a5ca98950a91 clarified access to antiquotation options;
wenzelm
parents: 67461
diff changeset
    74
(* output *)
a5ca98950a91 clarified access to antiquotation options;
wenzelm
parents: 67461
diff changeset
    75
70307
61e26527480e added document antiquotation option "cartouche";
wenzelm
parents: 69604
diff changeset
    76
fun delimit ctxt =
61e26527480e added document antiquotation option "cartouche";
wenzelm
parents: 69604
diff changeset
    77
  if Config.get ctxt thy_output_cartouche then Pretty.cartouche
61e26527480e added document antiquotation option "cartouche";
wenzelm
parents: 69604
diff changeset
    78
  else if Config.get ctxt thy_output_quotes then Pretty.quote
61e26527480e added document antiquotation option "cartouche";
wenzelm
parents: 69604
diff changeset
    79
  else I;
67464
a5ca98950a91 clarified access to antiquotation options;
wenzelm
parents: 67461
diff changeset
    80
a5ca98950a91 clarified access to antiquotation options;
wenzelm
parents: 67461
diff changeset
    81
fun indent ctxt =
a5ca98950a91 clarified access to antiquotation options;
wenzelm
parents: 67461
diff changeset
    82
  Config.get ctxt thy_output_display ? Pretty.indent (Config.get ctxt thy_output_indent);
a5ca98950a91 clarified access to antiquotation options;
wenzelm
parents: 67461
diff changeset
    83
a5ca98950a91 clarified access to antiquotation options;
wenzelm
parents: 67461
diff changeset
    84
fun format ctxt =
a5ca98950a91 clarified access to antiquotation options;
wenzelm
parents: 67461
diff changeset
    85
  if Config.get ctxt thy_output_display orelse Config.get ctxt thy_output_break
a5ca98950a91 clarified access to antiquotation options;
wenzelm
parents: 67461
diff changeset
    86
  then Pretty.string_of_margin (Config.get ctxt thy_output_margin)
a5ca98950a91 clarified access to antiquotation options;
wenzelm
parents: 67461
diff changeset
    87
  else Pretty.unformatted_string_of;
a5ca98950a91 clarified access to antiquotation options;
wenzelm
parents: 67461
diff changeset
    88
70307
61e26527480e added document antiquotation option "cartouche";
wenzelm
parents: 69604
diff changeset
    89
fun output ctxt = delimit ctxt #> indent ctxt #> format ctxt #> Output.output;
67464
a5ca98950a91 clarified access to antiquotation options;
wenzelm
parents: 67461
diff changeset
    90
a5ca98950a91 clarified access to antiquotation options;
wenzelm
parents: 67461
diff changeset
    91
67386
998e01d6f8fd clarified modules;
wenzelm
parents:
diff changeset
    92
(* theory data *)
998e01d6f8fd clarified modules;
wenzelm
parents:
diff changeset
    93
998e01d6f8fd clarified modules;
wenzelm
parents:
diff changeset
    94
structure Data = Theory_Data
998e01d6f8fd clarified modules;
wenzelm
parents:
diff changeset
    95
(
998e01d6f8fd clarified modules;
wenzelm
parents:
diff changeset
    96
  type T =
69604
a80d8ec6c998 support for isabelle update -u control_cartouches;
wenzelm
parents: 69359
diff changeset
    97
    (bool * (Token.src -> Proof.context -> Latex.text)) Name_Space.table *
67386
998e01d6f8fd clarified modules;
wenzelm
parents:
diff changeset
    98
      (string -> Proof.context -> Proof.context) Name_Space.table;
998e01d6f8fd clarified modules;
wenzelm
parents:
diff changeset
    99
  val empty : T =
998e01d6f8fd clarified modules;
wenzelm
parents:
diff changeset
   100
    (Name_Space.empty_table Markup.document_antiquotationN,
998e01d6f8fd clarified modules;
wenzelm
parents:
diff changeset
   101
      Name_Space.empty_table Markup.document_antiquotation_optionN);
998e01d6f8fd clarified modules;
wenzelm
parents:
diff changeset
   102
  val extend = I;
998e01d6f8fd clarified modules;
wenzelm
parents:
diff changeset
   103
  fun merge ((commands1, options1), (commands2, options2)) : T =
998e01d6f8fd clarified modules;
wenzelm
parents:
diff changeset
   104
    (Name_Space.merge_tables (commands1, commands2),
998e01d6f8fd clarified modules;
wenzelm
parents:
diff changeset
   105
      Name_Space.merge_tables (options1, options2));
998e01d6f8fd clarified modules;
wenzelm
parents:
diff changeset
   106
);
998e01d6f8fd clarified modules;
wenzelm
parents:
diff changeset
   107
998e01d6f8fd clarified modules;
wenzelm
parents:
diff changeset
   108
val get_antiquotations = Data.get o Proof_Context.theory_of;
998e01d6f8fd clarified modules;
wenzelm
parents:
diff changeset
   109
998e01d6f8fd clarified modules;
wenzelm
parents:
diff changeset
   110
fun print_antiquotations verbose ctxt =
998e01d6f8fd clarified modules;
wenzelm
parents:
diff changeset
   111
  let
998e01d6f8fd clarified modules;
wenzelm
parents:
diff changeset
   112
    val (commands, options) = get_antiquotations ctxt;
998e01d6f8fd clarified modules;
wenzelm
parents:
diff changeset
   113
    val command_names = map #1 (Name_Space.markup_table verbose ctxt commands);
998e01d6f8fd clarified modules;
wenzelm
parents:
diff changeset
   114
    val option_names = map #1 (Name_Space.markup_table verbose ctxt options);
998e01d6f8fd clarified modules;
wenzelm
parents:
diff changeset
   115
  in
998e01d6f8fd clarified modules;
wenzelm
parents:
diff changeset
   116
    [Pretty.big_list "document antiquotations:" (map Pretty.mark_str command_names),
998e01d6f8fd clarified modules;
wenzelm
parents:
diff changeset
   117
     Pretty.big_list "document antiquotation options:" (map Pretty.mark_str option_names)]
998e01d6f8fd clarified modules;
wenzelm
parents:
diff changeset
   118
  end |> Pretty.writeln_chunks;
998e01d6f8fd clarified modules;
wenzelm
parents:
diff changeset
   119
998e01d6f8fd clarified modules;
wenzelm
parents:
diff changeset
   120
fun check ctxt = #1 o Name_Space.check (Context.Proof ctxt) (#1 (get_antiquotations ctxt));
998e01d6f8fd clarified modules;
wenzelm
parents:
diff changeset
   121
fun check_option ctxt = #1 o Name_Space.check (Context.Proof ctxt) (#2 (get_antiquotations ctxt));
998e01d6f8fd clarified modules;
wenzelm
parents:
diff changeset
   122
69604
a80d8ec6c998 support for isabelle update -u control_cartouches;
wenzelm
parents: 69359
diff changeset
   123
fun gen_setup name embedded scan body thy =
67386
998e01d6f8fd clarified modules;
wenzelm
parents:
diff changeset
   124
  let
998e01d6f8fd clarified modules;
wenzelm
parents:
diff changeset
   125
    fun cmd src ctxt =
998e01d6f8fd clarified modules;
wenzelm
parents:
diff changeset
   126
      let val (x, ctxt') = Token.syntax scan src ctxt
67464
a5ca98950a91 clarified access to antiquotation options;
wenzelm
parents: 67461
diff changeset
   127
      in body {context = ctxt', source = src, argument = x} end;
69604
a80d8ec6c998 support for isabelle update -u control_cartouches;
wenzelm
parents: 69359
diff changeset
   128
    val entry = (name, (embedded, cmd));
a80d8ec6c998 support for isabelle update -u control_cartouches;
wenzelm
parents: 69359
diff changeset
   129
  in thy |> Data.map (apfst (Name_Space.define (Context.Theory thy) true entry #> #2)) end;
a80d8ec6c998 support for isabelle update -u control_cartouches;
wenzelm
parents: 69359
diff changeset
   130
a80d8ec6c998 support for isabelle update -u control_cartouches;
wenzelm
parents: 69359
diff changeset
   131
fun setup name = gen_setup name false;
a80d8ec6c998 support for isabelle update -u control_cartouches;
wenzelm
parents: 69359
diff changeset
   132
fun setup_embedded name = gen_setup name true;
67386
998e01d6f8fd clarified modules;
wenzelm
parents:
diff changeset
   133
998e01d6f8fd clarified modules;
wenzelm
parents:
diff changeset
   134
fun setup_option name opt thy = thy
998e01d6f8fd clarified modules;
wenzelm
parents:
diff changeset
   135
  |> Data.map (apsnd (Name_Space.define (Context.Theory thy) true (name, opt) #> #2));
998e01d6f8fd clarified modules;
wenzelm
parents:
diff changeset
   136
998e01d6f8fd clarified modules;
wenzelm
parents:
diff changeset
   137
998e01d6f8fd clarified modules;
wenzelm
parents:
diff changeset
   138
(* syntax *)
998e01d6f8fd clarified modules;
wenzelm
parents:
diff changeset
   139
998e01d6f8fd clarified modules;
wenzelm
parents:
diff changeset
   140
local
998e01d6f8fd clarified modules;
wenzelm
parents:
diff changeset
   141
998e01d6f8fd clarified modules;
wenzelm
parents:
diff changeset
   142
val property =
69359
7cef9e386ffe more accurate positions for "name" (quoted string) and "embedded" (cartouche): refer to content without delimiters, which is e.g. relevant for systematic selection/renaming of scope groups;
wenzelm
parents: 68223
diff changeset
   143
  Parse.name_position -- Scan.optional (Parse.$$$ "=" |-- Parse.!!! Parse.name) "";
67386
998e01d6f8fd clarified modules;
wenzelm
parents:
diff changeset
   144
998e01d6f8fd clarified modules;
wenzelm
parents:
diff changeset
   145
val properties =
998e01d6f8fd clarified modules;
wenzelm
parents:
diff changeset
   146
  Scan.optional (Parse.$$$ "[" |-- Parse.!!! (Parse.enum "," property --| Parse.$$$ "]")) [];
998e01d6f8fd clarified modules;
wenzelm
parents:
diff changeset
   147
998e01d6f8fd clarified modules;
wenzelm
parents:
diff changeset
   148
in
998e01d6f8fd clarified modules;
wenzelm
parents:
diff changeset
   149
67467
wenzelm
parents: 67464
diff changeset
   150
val parse_antiq =
67386
998e01d6f8fd clarified modules;
wenzelm
parents:
diff changeset
   151
  Parse.!!!
998e01d6f8fd clarified modules;
wenzelm
parents:
diff changeset
   152
    (Parse.token Parse.liberal_name -- properties -- Parse.args --| Scan.ahead Parse.eof)
69604
a80d8ec6c998 support for isabelle update -u control_cartouches;
wenzelm
parents: 69359
diff changeset
   153
  >> (fn ((name, opts), args) => (opts, name :: args));
67386
998e01d6f8fd clarified modules;
wenzelm
parents:
diff changeset
   154
998e01d6f8fd clarified modules;
wenzelm
parents:
diff changeset
   155
end;
998e01d6f8fd clarified modules;
wenzelm
parents:
diff changeset
   156
998e01d6f8fd clarified modules;
wenzelm
parents:
diff changeset
   157
998e01d6f8fd clarified modules;
wenzelm
parents:
diff changeset
   158
(* evaluate *)
998e01d6f8fd clarified modules;
wenzelm
parents:
diff changeset
   159
998e01d6f8fd clarified modules;
wenzelm
parents:
diff changeset
   160
local
998e01d6f8fd clarified modules;
wenzelm
parents:
diff changeset
   161
69604
a80d8ec6c998 support for isabelle update -u control_cartouches;
wenzelm
parents: 69359
diff changeset
   162
fun command pos (opts, src) ctxt =
a80d8ec6c998 support for isabelle update -u control_cartouches;
wenzelm
parents: 69359
diff changeset
   163
  let
a80d8ec6c998 support for isabelle update -u control_cartouches;
wenzelm
parents: 69359
diff changeset
   164
    val (src', (embedded, scan)) = Token.check_src ctxt (#1 o get_antiquotations) src;
a80d8ec6c998 support for isabelle update -u control_cartouches;
wenzelm
parents: 69359
diff changeset
   165
    val _ =
a80d8ec6c998 support for isabelle update -u control_cartouches;
wenzelm
parents: 69359
diff changeset
   166
      if null opts andalso Options.default_bool "update_control_cartouches" then
a80d8ec6c998 support for isabelle update -u control_cartouches;
wenzelm
parents: 69359
diff changeset
   167
        Context_Position.reports_text ctxt
a80d8ec6c998 support for isabelle update -u control_cartouches;
wenzelm
parents: 69359
diff changeset
   168
          (Antiquote.update_reports embedded pos (map Token.content_of src'))
a80d8ec6c998 support for isabelle update -u control_cartouches;
wenzelm
parents: 69359
diff changeset
   169
      else ();
a80d8ec6c998 support for isabelle update -u control_cartouches;
wenzelm
parents: 69359
diff changeset
   170
  in scan src' ctxt end;
67386
998e01d6f8fd clarified modules;
wenzelm
parents:
diff changeset
   171
998e01d6f8fd clarified modules;
wenzelm
parents:
diff changeset
   172
fun option ((xname, pos), s) ctxt =
998e01d6f8fd clarified modules;
wenzelm
parents:
diff changeset
   173
  let
998e01d6f8fd clarified modules;
wenzelm
parents:
diff changeset
   174
    val (_, opt) =
998e01d6f8fd clarified modules;
wenzelm
parents:
diff changeset
   175
      Name_Space.check (Context.Proof ctxt) (#2 (get_antiquotations ctxt)) (xname, pos);
998e01d6f8fd clarified modules;
wenzelm
parents:
diff changeset
   176
  in opt s ctxt end;
998e01d6f8fd clarified modules;
wenzelm
parents:
diff changeset
   177
69604
a80d8ec6c998 support for isabelle update -u control_cartouches;
wenzelm
parents: 69359
diff changeset
   178
fun eval ctxt pos (opts, src) =
67386
998e01d6f8fd clarified modules;
wenzelm
parents:
diff changeset
   179
  let
68223
88dd06301dd3 override default of Isabelle_Process, notably for PIDE export of "document.tex";
wenzelm
parents: 67571
diff changeset
   180
    val preview_ctxt = fold option opts (Config.put show_markup false ctxt);
69604
a80d8ec6c998 support for isabelle update -u control_cartouches;
wenzelm
parents: 69359
diff changeset
   181
    val _ = command pos (opts, src) preview_ctxt;
67473
7ed8d4cdfb13 recovered antiquotation check without latex mode (cf. dfc93f2b01ea);
wenzelm
parents: 67467
diff changeset
   182
67386
998e01d6f8fd clarified modules;
wenzelm
parents:
diff changeset
   183
    val print_ctxt = Context_Position.set_visible false preview_ctxt;
72305
9c0b835d4cc2 proper pretty printing for latex output, notably for pide_session=true (default);
wenzelm
parents: 70308
diff changeset
   184
    val print_modes =
9c0b835d4cc2 proper pretty printing for latex output, notably for pide_session=true (default);
wenzelm
parents: 70308
diff changeset
   185
      space_explode "," (Config.get print_ctxt thy_output_modes) @ [Latex.latexN, Pretty.regularN];
69604
a80d8ec6c998 support for isabelle update -u control_cartouches;
wenzelm
parents: 69359
diff changeset
   186
  in [Print_Mode.with_modes print_modes (fn () => command pos (opts, src) print_ctxt) ()] end;
67386
998e01d6f8fd clarified modules;
wenzelm
parents:
diff changeset
   187
998e01d6f8fd clarified modules;
wenzelm
parents:
diff changeset
   188
in
998e01d6f8fd clarified modules;
wenzelm
parents:
diff changeset
   189
67571
f858fe5531ac more uniform treatment of formal comments within document source;
wenzelm
parents: 67475
diff changeset
   190
fun evaluate eval_text ctxt antiq =
67467
wenzelm
parents: 67464
diff changeset
   191
  (case antiq of
67571
f858fe5531ac more uniform treatment of formal comments within document source;
wenzelm
parents: 67475
diff changeset
   192
    Antiquote.Text ss => eval_text ss
67467
wenzelm
parents: 67464
diff changeset
   193
  | Antiquote.Control {name, body, ...} =>
69604
a80d8ec6c998 support for isabelle update -u control_cartouches;
wenzelm
parents: 69359
diff changeset
   194
      eval ctxt Position.none
a80d8ec6c998 support for isabelle update -u control_cartouches;
wenzelm
parents: 69359
diff changeset
   195
        ([], Token.make_src name (if null body then [] else [Token.read_cartouche body]))
67467
wenzelm
parents: 67464
diff changeset
   196
  | Antiquote.Antiq {range = (pos, _), body, ...} =>
67386
998e01d6f8fd clarified modules;
wenzelm
parents:
diff changeset
   197
      let val keywords = Thy_Header.get_keywords' ctxt;
69604
a80d8ec6c998 support for isabelle update -u control_cartouches;
wenzelm
parents: 69359
diff changeset
   198
      in eval ctxt pos (Token.read_antiq keywords parse_antiq (body, pos)) end);
67386
998e01d6f8fd clarified modules;
wenzelm
parents:
diff changeset
   199
998e01d6f8fd clarified modules;
wenzelm
parents:
diff changeset
   200
end;
998e01d6f8fd clarified modules;
wenzelm
parents:
diff changeset
   201
998e01d6f8fd clarified modules;
wenzelm
parents:
diff changeset
   202
998e01d6f8fd clarified modules;
wenzelm
parents:
diff changeset
   203
(* option syntax *)
998e01d6f8fd clarified modules;
wenzelm
parents:
diff changeset
   204
998e01d6f8fd clarified modules;
wenzelm
parents:
diff changeset
   205
fun boolean "" = true
998e01d6f8fd clarified modules;
wenzelm
parents:
diff changeset
   206
  | boolean "true" = true
998e01d6f8fd clarified modules;
wenzelm
parents:
diff changeset
   207
  | boolean "false" = false
67464
a5ca98950a91 clarified access to antiquotation options;
wenzelm
parents: 67461
diff changeset
   208
  | boolean s = error ("Bad boolean value: " ^ Library.quote s);
67386
998e01d6f8fd clarified modules;
wenzelm
parents:
diff changeset
   209
998e01d6f8fd clarified modules;
wenzelm
parents:
diff changeset
   210
fun integer s =
998e01d6f8fd clarified modules;
wenzelm
parents:
diff changeset
   211
  let
998e01d6f8fd clarified modules;
wenzelm
parents:
diff changeset
   212
    fun int ss =
998e01d6f8fd clarified modules;
wenzelm
parents:
diff changeset
   213
      (case Library.read_int ss of (i, []) => i
67464
a5ca98950a91 clarified access to antiquotation options;
wenzelm
parents: 67461
diff changeset
   214
      | _ => error ("Bad integer value: " ^ Library.quote s));
67386
998e01d6f8fd clarified modules;
wenzelm
parents:
diff changeset
   215
  in (case Symbol.explode s of "-" :: ss => ~ (int ss) | ss => int ss) end;
998e01d6f8fd clarified modules;
wenzelm
parents:
diff changeset
   216
998e01d6f8fd clarified modules;
wenzelm
parents:
diff changeset
   217
val _ = Theory.setup
998e01d6f8fd clarified modules;
wenzelm
parents:
diff changeset
   218
 (setup_option \<^binding>\<open>show_types\<close> (Config.put show_types o boolean) #>
998e01d6f8fd clarified modules;
wenzelm
parents:
diff changeset
   219
  setup_option \<^binding>\<open>show_sorts\<close> (Config.put show_sorts o boolean) #>
998e01d6f8fd clarified modules;
wenzelm
parents:
diff changeset
   220
  setup_option \<^binding>\<open>show_structs\<close> (Config.put show_structs o boolean) #>
998e01d6f8fd clarified modules;
wenzelm
parents:
diff changeset
   221
  setup_option \<^binding>\<open>show_question_marks\<close> (Config.put show_question_marks o boolean) #>
998e01d6f8fd clarified modules;
wenzelm
parents:
diff changeset
   222
  setup_option \<^binding>\<open>show_abbrevs\<close> (Config.put show_abbrevs o boolean) #>
998e01d6f8fd clarified modules;
wenzelm
parents:
diff changeset
   223
  setup_option \<^binding>\<open>names_long\<close> (Config.put Name_Space.names_long o boolean) #>
998e01d6f8fd clarified modules;
wenzelm
parents:
diff changeset
   224
  setup_option \<^binding>\<open>names_short\<close> (Config.put Name_Space.names_short o boolean) #>
998e01d6f8fd clarified modules;
wenzelm
parents:
diff changeset
   225
  setup_option \<^binding>\<open>names_unique\<close> (Config.put Name_Space.names_unique o boolean) #>
998e01d6f8fd clarified modules;
wenzelm
parents:
diff changeset
   226
  setup_option \<^binding>\<open>eta_contract\<close> (Config.put Syntax_Trans.eta_contract o boolean) #>
998e01d6f8fd clarified modules;
wenzelm
parents:
diff changeset
   227
  setup_option \<^binding>\<open>display\<close> (Config.put thy_output_display o boolean) #>
998e01d6f8fd clarified modules;
wenzelm
parents:
diff changeset
   228
  setup_option \<^binding>\<open>break\<close> (Config.put thy_output_break o boolean) #>
70307
61e26527480e added document antiquotation option "cartouche";
wenzelm
parents: 69604
diff changeset
   229
  setup_option \<^binding>\<open>cartouche\<close> (Config.put thy_output_cartouche o boolean) #>
67386
998e01d6f8fd clarified modules;
wenzelm
parents:
diff changeset
   230
  setup_option \<^binding>\<open>quotes\<close> (Config.put thy_output_quotes o boolean) #>
67461
dfc93f2b01ea discontinued unused wrapper: print_mode is provided directly;
wenzelm
parents: 67386
diff changeset
   231
  setup_option \<^binding>\<open>mode\<close> (Config.put thy_output_modes) #>
67386
998e01d6f8fd clarified modules;
wenzelm
parents:
diff changeset
   232
  setup_option \<^binding>\<open>margin\<close> (Config.put thy_output_margin o integer) #>
998e01d6f8fd clarified modules;
wenzelm
parents:
diff changeset
   233
  setup_option \<^binding>\<open>indent\<close> (Config.put thy_output_indent o integer) #>
998e01d6f8fd clarified modules;
wenzelm
parents:
diff changeset
   234
  setup_option \<^binding>\<open>source\<close> (Config.put thy_output_source o boolean) #>
70308
a0b21b4b7a4a strip cartouches from arguments of "embedded" document antiquotations, corresponding to automated update via "isabelle update -u control_cartouches" -- e.g. relevant for documents with thy_output_source (e.g. doc "isar-ref", "jedit", "system");
wenzelm
parents: 70307
diff changeset
   235
  setup_option \<^binding>\<open>source_cartouche\<close> (Config.put thy_output_source_cartouche o boolean) #>
67386
998e01d6f8fd clarified modules;
wenzelm
parents:
diff changeset
   236
  setup_option \<^binding>\<open>goals_limit\<close> (Config.put Goal_Display.goals_limit o integer));
998e01d6f8fd clarified modules;
wenzelm
parents:
diff changeset
   237
998e01d6f8fd clarified modules;
wenzelm
parents:
diff changeset
   238
end;