src/Pure/Thy/thy_output.ML
author wenzelm
Tue, 25 Feb 2014 10:50:12 +0100
changeset 55739 d8270c17b5be
parent 55614 e2d71b8b0d95
child 55743 225a060e7445
permissions -rw-r--r--
more markup;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
22124
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
     1
(*  Title:      Pure/Thy/thy_output.ML
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
     2
    Author:     Markus Wenzel, TU Muenchen
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
     3
30390
ad591ee76c78 simplified interface to define document antiquotations, cf. antiquotatation, maybe_pretty_source, output;
wenzelm
parents: 30381
diff changeset
     4
Theory document output with antiquotations.
22124
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
     5
*)
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
     6
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
     7
signature THY_OUTPUT =
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
     8
sig
38767
d8da44a8dd25 proper context for various Thy_Output options, via official configuration options in ML and Isar;
wenzelm
parents: 38766
diff changeset
     9
  val display: bool Config.T
d8da44a8dd25 proper context for various Thy_Output options, via official configuration options in ML and Isar;
wenzelm
parents: 38766
diff changeset
    10
  val quotes: bool Config.T
d8da44a8dd25 proper context for various Thy_Output options, via official configuration options in ML and Isar;
wenzelm
parents: 38766
diff changeset
    11
  val indent: int Config.T
d8da44a8dd25 proper context for various Thy_Output options, via official configuration options in ML and Isar;
wenzelm
parents: 38766
diff changeset
    12
  val source: bool Config.T
d8da44a8dd25 proper context for various Thy_Output options, via official configuration options in ML and Isar;
wenzelm
parents: 38766
diff changeset
    13
  val break: bool Config.T
52042
aae07a3ff536 Thy_Output.modes as proper option;
wenzelm
parents: 52041
diff changeset
    14
  val modes: string Config.T
38766
8891f4520d16 Thy_Output: options based on proper context, although Thy_Output.add_wrapper still allows to maintain old-style wrapper combinators (setmp_CRITICAL etc.);
wenzelm
parents: 37216
diff changeset
    15
  val add_wrapper: ((unit -> string) -> unit -> string) -> Proof.context -> Proof.context
43564
9864182c6bad document antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents: 42669
diff changeset
    16
  val add_option: binding -> (string -> Proof.context -> Proof.context) -> theory -> theory
53044
be27b6be8027 more markup via Name_Space.check;
wenzelm
parents: 52042
diff changeset
    17
  val check_command: theory -> xstring * Position.T -> string
be27b6be8027 more markup via Name_Space.check;
wenzelm
parents: 52042
diff changeset
    18
  val check_option: theory -> xstring * Position.T -> string
43564
9864182c6bad document antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents: 42669
diff changeset
    19
  val print_antiquotations: Proof.context -> unit
9864182c6bad document antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents: 42669
diff changeset
    20
  val antiquotation: binding -> 'a context_parser ->
9864182c6bad document antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents: 42669
diff changeset
    21
    ({source: Args.src, state: Toplevel.state, context: Proof.context} -> 'a -> string) ->
9864182c6bad document antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents: 42669
diff changeset
    22
      theory -> theory
22124
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
    23
  val boolean: string -> bool
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
    24
  val integer: string -> int
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
    25
  datatype markup = Markup | MarkupEnv | Verbatim
55526
39708e59f4b0 more markup;
wenzelm
parents: 55111
diff changeset
    26
  val eval_antiq: Scan.lexicon -> Toplevel.state -> Antiquote.antiq -> string
30573
49899f26fbd1 de-camelized Symbol_Pos;
wenzelm
parents: 30513
diff changeset
    27
  val eval_antiquote: Scan.lexicon -> Toplevel.state -> Symbol_Pos.text * Position.T -> string
48918
6e5fd4585512 check side-comments of command spans (normally filtered out in Outer_Syntax.toplevel_source);
wenzelm
parents: 47005
diff changeset
    28
  val check_text: Symbol_Pos.text * Position.T -> Toplevel.state -> unit
28427
cc9f7d99fb73 turned process_thy into present_thy, which merely does presentation (wrt. persistent intermediate states);
wenzelm
parents: 28273
diff changeset
    29
  val present_thy: Scan.lexicon -> (string -> string list) -> (markup -> string -> bool) ->
46811
03a2dc9e0624 clarified command span: include trailing whitespace/comments and thus reduce number of ignored spans with associated transactions and states (factor 2);
wenzelm
parents: 46261
diff changeset
    30
    (Toplevel.transition * Toplevel.state) list -> Token.T list -> Buffer.T
38767
d8da44a8dd25 proper context for various Thy_Output options, via official configuration options in ML and Isar;
wenzelm
parents: 38766
diff changeset
    31
  val pretty_text: Proof.context -> string -> Pretty.T
28644
e2ae4a6cf166 ThyOutput: export some auxiliary operations;
wenzelm
parents: 28427
diff changeset
    32
  val pretty_term: Proof.context -> term -> Pretty.T
e2ae4a6cf166 ThyOutput: export some auxiliary operations;
wenzelm
parents: 28427
diff changeset
    33
  val pretty_thm: Proof.context -> thm -> Pretty.T
30390
ad591ee76c78 simplified interface to define document antiquotations, cf. antiquotatation, maybe_pretty_source, output;
wenzelm
parents: 30381
diff changeset
    34
  val str_of_source: Args.src -> string
38767
d8da44a8dd25 proper context for various Thy_Output options, via official configuration options in ML and Isar;
wenzelm
parents: 38766
diff changeset
    35
  val maybe_pretty_source: (Proof.context -> 'a -> Pretty.T) -> Proof.context ->
d8da44a8dd25 proper context for various Thy_Output options, via official configuration options in ML and Isar;
wenzelm
parents: 38766
diff changeset
    36
    Args.src -> 'a list -> Pretty.T list
d8da44a8dd25 proper context for various Thy_Output options, via official configuration options in ML and Isar;
wenzelm
parents: 38766
diff changeset
    37
  val output: Proof.context -> Pretty.T list -> string
49244
fb669aff821e formal markup for @{file} (for hyperlinks etc.) -- interpret path wrt. master directory as usual;
wenzelm
parents: 48992
diff changeset
    38
  val verb_text: string -> string
22124
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
    39
end;
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
    40
37216
3165bc303f66 modernized some structure names, keeping a few legacy aliases;
wenzelm
parents: 37198
diff changeset
    41
structure Thy_Output: THY_OUTPUT =
22124
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
    42
struct
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
    43
52042
aae07a3ff536 Thy_Output.modes as proper option;
wenzelm
parents: 52041
diff changeset
    44
(** options **)
22124
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
    45
52041
80e001b85332 some system options as context-sensitive config options;
wenzelm
parents: 51958
diff changeset
    46
val display = Attrib.setup_option_bool "thy_output_display";
80e001b85332 some system options as context-sensitive config options;
wenzelm
parents: 51958
diff changeset
    47
val break = Attrib.setup_option_bool "thy_output_break";
80e001b85332 some system options as context-sensitive config options;
wenzelm
parents: 51958
diff changeset
    48
val quotes = Attrib.setup_option_bool "thy_output_quotes";
80e001b85332 some system options as context-sensitive config options;
wenzelm
parents: 51958
diff changeset
    49
val indent = Attrib.setup_option_int "thy_output_indent";
80e001b85332 some system options as context-sensitive config options;
wenzelm
parents: 51958
diff changeset
    50
val source = Attrib.setup_option_bool "thy_output_source";
52042
aae07a3ff536 Thy_Output.modes as proper option;
wenzelm
parents: 52041
diff changeset
    51
val modes = Attrib.setup_option_string "thy_output_modes";
22124
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
    52
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
    53
38766
8891f4520d16 Thy_Output: options based on proper context, although Thy_Output.add_wrapper still allows to maintain old-style wrapper combinators (setmp_CRITICAL etc.);
wenzelm
parents: 37216
diff changeset
    54
structure Wrappers = Proof_Data
8891f4520d16 Thy_Output: options based on proper context, although Thy_Output.add_wrapper still allows to maintain old-style wrapper combinators (setmp_CRITICAL etc.);
wenzelm
parents: 37216
diff changeset
    55
(
8891f4520d16 Thy_Output: options based on proper context, although Thy_Output.add_wrapper still allows to maintain old-style wrapper combinators (setmp_CRITICAL etc.);
wenzelm
parents: 37216
diff changeset
    56
  type T = ((unit -> string) -> unit -> string) list;
8891f4520d16 Thy_Output: options based on proper context, although Thy_Output.add_wrapper still allows to maintain old-style wrapper combinators (setmp_CRITICAL etc.);
wenzelm
parents: 37216
diff changeset
    57
  fun init _ = [];
8891f4520d16 Thy_Output: options based on proper context, although Thy_Output.add_wrapper still allows to maintain old-style wrapper combinators (setmp_CRITICAL etc.);
wenzelm
parents: 37216
diff changeset
    58
);
8891f4520d16 Thy_Output: options based on proper context, although Thy_Output.add_wrapper still allows to maintain old-style wrapper combinators (setmp_CRITICAL etc.);
wenzelm
parents: 37216
diff changeset
    59
8891f4520d16 Thy_Output: options based on proper context, although Thy_Output.add_wrapper still allows to maintain old-style wrapper combinators (setmp_CRITICAL etc.);
wenzelm
parents: 37216
diff changeset
    60
fun add_wrapper wrapper = Wrappers.map (cons wrapper);
8891f4520d16 Thy_Output: options based on proper context, although Thy_Output.add_wrapper still allows to maintain old-style wrapper combinators (setmp_CRITICAL etc.);
wenzelm
parents: 37216
diff changeset
    61
8891f4520d16 Thy_Output: options based on proper context, although Thy_Output.add_wrapper still allows to maintain old-style wrapper combinators (setmp_CRITICAL etc.);
wenzelm
parents: 37216
diff changeset
    62
val wrap = Wrappers.get #> fold (fn wrapper => fn f => wrapper f);
8891f4520d16 Thy_Output: options based on proper context, although Thy_Output.add_wrapper still allows to maintain old-style wrapper combinators (setmp_CRITICAL etc.);
wenzelm
parents: 37216
diff changeset
    63
8891f4520d16 Thy_Output: options based on proper context, although Thy_Output.add_wrapper still allows to maintain old-style wrapper combinators (setmp_CRITICAL etc.);
wenzelm
parents: 37216
diff changeset
    64
22124
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
    65
30390
ad591ee76c78 simplified interface to define document antiquotations, cf. antiquotatation, maybe_pretty_source, output;
wenzelm
parents: 30381
diff changeset
    66
(** maintain global antiquotations **)
22124
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
    67
43564
9864182c6bad document antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents: 42669
diff changeset
    68
structure Antiquotations = Theory_Data
9864182c6bad document antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents: 42669
diff changeset
    69
(
9864182c6bad document antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents: 42669
diff changeset
    70
  type T =
9864182c6bad document antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents: 42669
diff changeset
    71
    (Args.src -> Toplevel.state -> Proof.context -> string) Name_Space.table *
9864182c6bad document antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents: 42669
diff changeset
    72
      (string -> Proof.context -> Proof.context) Name_Space.table;
9864182c6bad document antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents: 42669
diff changeset
    73
  val empty : T =
50201
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49847
diff changeset
    74
    (Name_Space.empty_table Markup.document_antiquotationN,
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49847
diff changeset
    75
      Name_Space.empty_table Markup.document_antiquotation_optionN);
43564
9864182c6bad document antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents: 42669
diff changeset
    76
  val extend = I;
9864182c6bad document antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents: 42669
diff changeset
    77
  fun merge ((commands1, options1), (commands2, options2)) : T =
9864182c6bad document antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents: 42669
diff changeset
    78
    (Name_Space.merge_tables (commands1, commands2),
9864182c6bad document antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents: 42669
diff changeset
    79
      Name_Space.merge_tables (options1, options2));
9864182c6bad document antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents: 42669
diff changeset
    80
);
22124
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
    81
47005
421760a1efe7 maintain generic context naming in structure Name_Space (NB: empty = default_naming, init = local_naming);
wenzelm
parents: 46958
diff changeset
    82
fun add_command name cmd thy = thy
421760a1efe7 maintain generic context naming in structure Name_Space (NB: empty = default_naming, init = local_naming);
wenzelm
parents: 46958
diff changeset
    83
  |> Antiquotations.map (apfst (Name_Space.define (Context.Theory thy) true (name, cmd) #> snd));
22124
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
    84
47005
421760a1efe7 maintain generic context naming in structure Name_Space (NB: empty = default_naming, init = local_naming);
wenzelm
parents: 46958
diff changeset
    85
fun add_option name opt thy = thy
421760a1efe7 maintain generic context naming in structure Name_Space (NB: empty = default_naming, init = local_naming);
wenzelm
parents: 46958
diff changeset
    86
  |> Antiquotations.map (apsnd (Name_Space.define (Context.Theory thy) true (name, opt) #> snd));
22124
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
    87
53044
be27b6be8027 more markup via Name_Space.check;
wenzelm
parents: 52042
diff changeset
    88
fun check_command thy = #1 o Name_Space.check (Context.Theory thy) (#1 (Antiquotations.get thy));
26893
44d9960d3587 added defined_command, defined_option;
wenzelm
parents: 26762
diff changeset
    89
53044
be27b6be8027 more markup via Name_Space.check;
wenzelm
parents: 52042
diff changeset
    90
fun check_option thy = #1 o Name_Space.check (Context.Theory thy) (#2 (Antiquotations.get thy));
43564
9864182c6bad document antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents: 42669
diff changeset
    91
9864182c6bad document antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents: 42669
diff changeset
    92
fun command src state ctxt =
9864182c6bad document antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents: 42669
diff changeset
    93
  let
9864182c6bad document antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents: 42669
diff changeset
    94
    val thy = Proof_Context.theory_of ctxt;
9864182c6bad document antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents: 42669
diff changeset
    95
    val ((xname, _), pos) = Args.dest_src src;
47005
421760a1efe7 maintain generic context naming in structure Name_Space (NB: empty = default_naming, init = local_naming);
wenzelm
parents: 46958
diff changeset
    96
    val (name, f) = Name_Space.check (Context.Proof ctxt) (#1 (Antiquotations.get thy)) (xname, pos);
43564
9864182c6bad document antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents: 42669
diff changeset
    97
  in
9864182c6bad document antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents: 42669
diff changeset
    98
    f src state ctxt handle ERROR msg =>
9864182c6bad document antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents: 42669
diff changeset
    99
      cat_error msg ("The error(s) above occurred in document antiquotation: " ^
48992
0518bf89c777 renamed Position.str_of to Position.here;
wenzelm
parents: 48927
diff changeset
   100
        quote name ^ Position.here pos)
22124
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
   101
  end;
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
   102
43564
9864182c6bad document antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents: 42669
diff changeset
   103
fun option ((xname, pos), s) ctxt =
9864182c6bad document antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents: 42669
diff changeset
   104
  let
9864182c6bad document antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents: 42669
diff changeset
   105
    val thy = Proof_Context.theory_of ctxt;
47005
421760a1efe7 maintain generic context naming in structure Name_Space (NB: empty = default_naming, init = local_naming);
wenzelm
parents: 46958
diff changeset
   106
    val (_, opt) = Name_Space.check (Context.Proof ctxt) (#2 (Antiquotations.get thy)) (xname, pos);
43564
9864182c6bad document antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents: 42669
diff changeset
   107
  in opt s ctxt end;
22124
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
   108
43564
9864182c6bad document antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents: 42669
diff changeset
   109
fun print_antiquotations ctxt =
9864182c6bad document antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents: 42669
diff changeset
   110
  let
9864182c6bad document antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents: 42669
diff changeset
   111
    val thy = Proof_Context.theory_of ctxt;
9864182c6bad document antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents: 42669
diff changeset
   112
    val (commands, options) = Antiquotations.get thy;
9864182c6bad document antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents: 42669
diff changeset
   113
    val command_names = map #1 (Name_Space.extern_table ctxt commands);
9864182c6bad document antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents: 42669
diff changeset
   114
    val option_names = map #1 (Name_Space.extern_table ctxt options);
9864182c6bad document antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents: 42669
diff changeset
   115
  in
50301
56b4c9afd7be print formal entities with markup;
wenzelm
parents: 50201
diff changeset
   116
    [Pretty.big_list "document antiquotations:" (map Pretty.mark_str command_names),
56b4c9afd7be print formal entities with markup;
wenzelm
parents: 50201
diff changeset
   117
      Pretty.big_list "document antiquotation options:" (map Pretty.mark_str option_names)]
43564
9864182c6bad document antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents: 42669
diff changeset
   118
    |> Pretty.chunks |> Pretty.writeln
9864182c6bad document antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents: 42669
diff changeset
   119
  end;
22124
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
   120
38766
8891f4520d16 Thy_Output: options based on proper context, although Thy_Output.add_wrapper still allows to maintain old-style wrapper combinators (setmp_CRITICAL etc.);
wenzelm
parents: 37216
diff changeset
   121
fun antiquotation name scan out =
8891f4520d16 Thy_Output: options based on proper context, although Thy_Output.add_wrapper still allows to maintain old-style wrapper combinators (setmp_CRITICAL etc.);
wenzelm
parents: 37216
diff changeset
   122
  add_command name
8891f4520d16 Thy_Output: options based on proper context, although Thy_Output.add_wrapper still allows to maintain old-style wrapper combinators (setmp_CRITICAL etc.);
wenzelm
parents: 37216
diff changeset
   123
    (fn src => fn state => fn ctxt =>
8891f4520d16 Thy_Output: options based on proper context, although Thy_Output.add_wrapper still allows to maintain old-style wrapper combinators (setmp_CRITICAL etc.);
wenzelm
parents: 37216
diff changeset
   124
      let val (x, ctxt') = Args.context_syntax "document antiquotation" scan src ctxt
8891f4520d16 Thy_Output: options based on proper context, although Thy_Output.add_wrapper still allows to maintain old-style wrapper combinators (setmp_CRITICAL etc.);
wenzelm
parents: 37216
diff changeset
   125
      in out {source = src, state = state, context = ctxt'} x end);
30390
ad591ee76c78 simplified interface to define document antiquotations, cf. antiquotatation, maybe_pretty_source, output;
wenzelm
parents: 30381
diff changeset
   126
22124
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
   127
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
   128
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
   129
(** syntax of antiquotations **)
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
   130
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
   131
(* option values *)
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
   132
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
   133
fun boolean "" = true
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
   134
  | boolean "true" = true
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
   135
  | boolean "false" = false
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
   136
  | boolean s = error ("Bad boolean value: " ^ quote s);
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
   137
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
   138
fun integer s =
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
   139
  let
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
   140
    fun int ss =
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
   141
      (case Library.read_int ss of (i, []) => i
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
   142
      | _ => error ("Bad integer value: " ^ quote s));
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
   143
  in (case Symbol.explode s of "-" :: ss => ~ (int ss) | ss => int ss) end;
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
   144
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
   145
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
   146
(* outer syntax *)
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
   147
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
   148
local
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
   149
36950
75b8f26f2f07 refer directly to structure Keyword and Parse;
wenzelm
parents: 36745
diff changeset
   150
val property =
43564
9864182c6bad document antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents: 42669
diff changeset
   151
  Parse.position Parse.xname -- Scan.optional (Parse.$$$ "=" |-- Parse.!!! Parse.xname) "";
36950
75b8f26f2f07 refer directly to structure Keyword and Parse;
wenzelm
parents: 36745
diff changeset
   152
75b8f26f2f07 refer directly to structure Keyword and Parse;
wenzelm
parents: 36745
diff changeset
   153
val properties =
75b8f26f2f07 refer directly to structure Keyword and Parse;
wenzelm
parents: 36745
diff changeset
   154
  Scan.optional (Parse.$$$ "[" |-- Parse.!!! (Parse.enum "," property --| Parse.$$$ "]")) [];
22124
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
   155
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
   156
in
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
   157
36950
75b8f26f2f07 refer directly to structure Keyword and Parse;
wenzelm
parents: 36745
diff changeset
   158
val antiq =
40800
330eb65c9469 Parse.liberal_name for document antiquotations and attributes;
wenzelm
parents: 39689
diff changeset
   159
  Parse.!!!
330eb65c9469 Parse.liberal_name for document antiquotations and attributes;
wenzelm
parents: 39689
diff changeset
   160
    (Parse.position Parse.liberal_name -- properties -- Args.parse --| Scan.ahead Parse.eof)
22124
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
   161
  >> (fn (((x, pos), y), z) => (y, Args.src ((x, z), pos)));
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
   162
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
   163
end;
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
   164
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
   165
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
   166
(* eval_antiquote *)
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
   167
55526
39708e59f4b0 more markup;
wenzelm
parents: 55111
diff changeset
   168
fun eval_antiq lex state ((ss, {range = (pos, _), ...}): Antiquote.antiq) =
42508
e21362bf1d93 allow nested @{antiq} (nonterminal) and @@{antiq} terminal;
wenzelm
parents: 42399
diff changeset
   169
  let
e21362bf1d93 allow nested @{antiq} (nonterminal) and @@{antiq} terminal;
wenzelm
parents: 42399
diff changeset
   170
    val (opts, src) = Token.read_antiq lex antiq (ss, pos);
e21362bf1d93 allow nested @{antiq} (nonterminal) and @@{antiq} terminal;
wenzelm
parents: 42399
diff changeset
   171
    fun cmd ctxt = wrap ctxt (fn () => command src state ctxt) ();
e21362bf1d93 allow nested @{antiq} (nonterminal) and @@{antiq} terminal;
wenzelm
parents: 42399
diff changeset
   172
    val preview_ctxt = fold option opts (Toplevel.presentation_context_of state);
e21362bf1d93 allow nested @{antiq} (nonterminal) and @@{antiq} terminal;
wenzelm
parents: 42399
diff changeset
   173
    val print_ctxt = Context_Position.set_visible false preview_ctxt;
e21362bf1d93 allow nested @{antiq} (nonterminal) and @@{antiq} terminal;
wenzelm
parents: 42399
diff changeset
   174
    val _ = cmd preview_ctxt;
52042
aae07a3ff536 Thy_Output.modes as proper option;
wenzelm
parents: 52041
diff changeset
   175
    val print_modes = space_explode "," (Config.get print_ctxt modes) @ Latex.modes;
aae07a3ff536 Thy_Output.modes as proper option;
wenzelm
parents: 52041
diff changeset
   176
  in Print_Mode.with_modes print_modes (fn () => cmd print_ctxt) () end;
42508
e21362bf1d93 allow nested @{antiq} (nonterminal) and @@{antiq} terminal;
wenzelm
parents: 42399
diff changeset
   177
30367
ee8841b1b981 simplified presentation: pass state directly;
wenzelm
parents: 30317
diff changeset
   178
fun eval_antiquote lex state (txt, pos) =
22124
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
   179
  let
30589
cbe27c4ef417 Antiquote.Text: keep full position information;
wenzelm
parents: 30588
diff changeset
   180
    fun expand (Antiquote.Text ss) = Symbol_Pos.content ss
53167
4e7ddd76e632 discontinued unused antiquotation blocks;
wenzelm
parents: 53044
diff changeset
   181
      | expand (Antiquote.Antiq antiq) = eval_antiq lex state antiq;
30642
0c9f9c49d5df simplified Antiquote.read (again);
wenzelm
parents: 30635
diff changeset
   182
    val ants = Antiquote.read (Symbol_Pos.explode (txt, pos), pos);
22124
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
   183
  in
30635
a7d175c48228 replaced Antiquote.is_antiq by Antiquote.is_text;
wenzelm
parents: 30613
diff changeset
   184
    if Toplevel.is_toplevel state andalso not (forall Antiquote.is_text ants) then
48992
0518bf89c777 renamed Position.str_of to Position.here;
wenzelm
parents: 48927
diff changeset
   185
      error ("Unknown context -- cannot expand document antiquotations" ^ Position.here pos)
22124
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
   186
    else implode (map expand ants)
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
   187
  end;
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
   188
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
   189
48918
6e5fd4585512 check side-comments of command spans (normally filtered out in Outer_Syntax.toplevel_source);
wenzelm
parents: 47005
diff changeset
   190
fun check_text (txt, pos) state =
55550
bcc643ac071a generic markup for embedded languages;
wenzelm
parents: 55526
diff changeset
   191
 (Position.report pos Markup.language_document;
51556
7ada6dfa9ab5 more liberal handling of skipped proofs;
wenzelm
parents: 51267
diff changeset
   192
  if Toplevel.is_skipped_proof state then ()
7ada6dfa9ab5 more liberal handling of skipped proofs;
wenzelm
parents: 51267
diff changeset
   193
  else ignore (eval_antiquote (#1 (Keyword.get_lexicons ())) state (txt, pos)));
48918
6e5fd4585512 check side-comments of command spans (normally filtered out in Outer_Syntax.toplevel_source);
wenzelm
parents: 47005
diff changeset
   194
6e5fd4585512 check side-comments of command spans (normally filtered out in Outer_Syntax.toplevel_source);
wenzelm
parents: 47005
diff changeset
   195
22124
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
   196
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
   197
(** present theory source **)
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
   198
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
   199
(*NB: arranging white space around command spans is a black art.*)
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
   200
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
   201
(* presentation tokens *)
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
   202
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
   203
datatype token =
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
   204
    NoToken
36959
f5417836dbea renamed structure OuterLex to Token and type token to Token.T, keeping legacy aliases for some time;
wenzelm
parents: 36950
diff changeset
   205
  | BasicToken of Token.T
22124
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
   206
  | MarkupToken of string * (string * Position.T)
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
   207
  | MarkupEnvToken of string * (string * Position.T)
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
   208
  | VerbatimToken of string * Position.T;
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
   209
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
   210
fun output_token lex state =
30367
ee8841b1b981 simplified presentation: pass state directly;
wenzelm
parents: 30317
diff changeset
   211
  let val eval = eval_antiquote lex state in
22124
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
   212
    fn NoToken => ""
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
   213
     | BasicToken tok => Latex.output_basic tok
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
   214
     | MarkupToken (cmd, txt) => Latex.output_markup cmd (eval txt)
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
   215
     | MarkupEnvToken (cmd, txt) => Latex.output_markup_env cmd (eval txt)
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
   216
     | VerbatimToken txt => Latex.output_verbatim (eval txt)
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
   217
  end;
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
   218
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
   219
fun basic_token pred (BasicToken tok) = pred tok
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
   220
  | basic_token _ _ = false;
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
   221
51267
wenzelm
parents: 50592
diff changeset
   222
val improper_token = basic_token Token.is_improper;
36959
f5417836dbea renamed structure OuterLex to Token and type token to Token.T, keeping legacy aliases for some time;
wenzelm
parents: 36950
diff changeset
   223
val comment_token = basic_token Token.is_comment;
f5417836dbea renamed structure OuterLex to Token and type token to Token.T, keeping legacy aliases for some time;
wenzelm
parents: 36950
diff changeset
   224
val blank_token = basic_token Token.is_blank;
f5417836dbea renamed structure OuterLex to Token and type token to Token.T, keeping legacy aliases for some time;
wenzelm
parents: 36950
diff changeset
   225
val newline_token = basic_token Token.is_newline;
22124
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
   226
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
   227
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
   228
(* command spans *)
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
   229
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
   230
type command = string * Position.T * string list;   (*name, position, tags*)
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
   231
type source = (token * (string * int)) list;        (*token, markup flag, meta-comment depth*)
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
   232
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
   233
datatype span = Span of command * (source * source * source * source) * bool;
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
   234
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
   235
fun make_span cmd src =
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
   236
  let
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
   237
    fun take_newline (tok :: toks) =
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
   238
          if newline_token (fst tok) then ([tok], toks, true)
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
   239
          else ([], tok :: toks, false)
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
   240
      | take_newline [] = ([], [], false);
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
   241
    val (((src_prefix, src_main), src_suffix1), (src_suffix2, src_appendix, newline)) =
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
   242
      src
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
   243
      |> take_prefix (improper_token o fst)
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
   244
      ||>> take_suffix (improper_token o fst)
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
   245
      ||>> take_prefix (comment_token o fst)
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
   246
      ||> take_newline;
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
   247
  in Span (cmd, (src_prefix, src_main, src_suffix1 @ src_suffix2, src_appendix), newline) end;
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
   248
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
   249
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
   250
(* present spans *)
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
   251
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
   252
local
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
   253
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
   254
fun err_bad_nesting pos =
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
   255
  error ("Bad nesting of commands in presentation" ^ pos);
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
   256
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
   257
fun edge which f (x: string option, y) =
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
   258
  if x = y then I
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
   259
  else (case which (x, y) of NONE => I | SOME txt => Buffer.add (f txt));
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
   260
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
   261
val begin_tag = edge #2 Latex.begin_tag;
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
   262
val end_tag = edge #1 Latex.end_tag;
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
   263
fun open_delim delim e = edge #2 Latex.begin_delim e #> delim #> edge #2 Latex.end_delim e;
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
   264
fun close_delim delim e = edge #1 Latex.begin_delim e #> delim #> edge #1 Latex.end_delim e;
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
   265
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
   266
in
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
   267
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
   268
fun present_span lex default_tags span state state'
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
   269
    (tag_stack, active_tag, newline, buffer, present_cont) =
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
   270
  let
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
   271
    val present = fold (fn (tok, (flag, 0)) =>
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
   272
        Buffer.add (output_token lex state' tok)
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
   273
        #> Buffer.add flag
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
   274
      | _ => I);
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
   275
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
   276
    val Span ((cmd_name, cmd_pos, cmd_tags), srcs, span_newline) = span;
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
   277
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
   278
    val (tag, tags) = tag_stack;
46924
wenzelm
parents: 46922
diff changeset
   279
    val tag' = try hd (fold (update (op =)) cmd_tags (the_list tag));
22124
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
   280
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
   281
    val active_tag' =
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
   282
      if is_some tag' then tag'
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
   283
      else if cmd_name = "end" andalso not (Toplevel.is_toplevel state') then NONE
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
   284
      else try hd (default_tags cmd_name);
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
   285
    val edge = (active_tag, active_tag');
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
   286
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
   287
    val newline' =
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
   288
      if is_none active_tag' then span_newline else newline;
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
   289
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
   290
    val nesting = Toplevel.level state' - Toplevel.level state;
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
   291
    val tag_stack' =
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
   292
      if nesting = 0 andalso not (Toplevel.is_proof state) then tag_stack
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
   293
      else if nesting >= 0 then (tag', replicate nesting tag @ tags)
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
   294
      else
33957
e9afca2118d4 normalized uncurry take/drop
haftmann
parents: 33955
diff changeset
   295
        (case drop (~ nesting - 1) tags of
22124
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
   296
          tgs :: tgss => (tgs, tgss)
48992
0518bf89c777 renamed Position.str_of to Position.here;
wenzelm
parents: 48927
diff changeset
   297
        | [] => err_bad_nesting (Position.here cmd_pos));
22124
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
   298
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
   299
    val buffer' =
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
   300
      buffer
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
   301
      |> end_tag edge
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
   302
      |> close_delim (fst present_cont) edge
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
   303
      |> snd present_cont
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
   304
      |> open_delim (present (#1 srcs)) edge
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
   305
      |> begin_tag edge
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
   306
      |> present (#2 srcs);
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
   307
    val present_cont' =
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
   308
      if newline then (present (#3 srcs), present (#4 srcs))
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
   309
      else (I, present (#3 srcs) #> present (#4 srcs));
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
   310
  in (tag_stack', active_tag', newline', buffer', present_cont') end;
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
   311
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
   312
fun present_trailer ((_, tags), active_tag, _, buffer, present_cont) =
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
   313
  if not (null tags) then err_bad_nesting " at end of theory"
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
   314
  else
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
   315
    buffer
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
   316
    |> end_tag (active_tag, NONE)
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
   317
    |> close_delim (fst present_cont) (active_tag, NONE)
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
   318
    |> snd present_cont;
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
   319
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
   320
end;
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
   321
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
   322
28427
cc9f7d99fb73 turned process_thy into present_thy, which merely does presentation (wrt. persistent intermediate states);
wenzelm
parents: 28273
diff changeset
   323
(* present_thy *)
22124
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
   324
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
   325
datatype markup = Markup | MarkupEnv | Verbatim;
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
   326
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
   327
local
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
   328
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
   329
val space_proper =
36959
f5417836dbea renamed structure OuterLex to Token and type token to Token.T, keeping legacy aliases for some time;
wenzelm
parents: 36950
diff changeset
   330
  Scan.one Token.is_blank -- Scan.many Token.is_comment -- Scan.one Token.is_proper;
22124
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
   331
36959
f5417836dbea renamed structure OuterLex to Token and type token to Token.T, keeping legacy aliases for some time;
wenzelm
parents: 36950
diff changeset
   332
val is_improper = not o (Token.is_proper orf Token.is_begin_ignore orf Token.is_end_ignore);
22124
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
   333
val improper = Scan.many is_improper;
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
   334
val improper_end = Scan.repeat (Scan.unless space_proper (Scan.one is_improper));
36959
f5417836dbea renamed structure OuterLex to Token and type token to Token.T, keeping legacy aliases for some time;
wenzelm
parents: 36950
diff changeset
   335
val blank_end = Scan.repeat (Scan.unless space_proper (Scan.one Token.is_blank));
22124
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
   336
36959
f5417836dbea renamed structure OuterLex to Token and type token to Token.T, keeping legacy aliases for some time;
wenzelm
parents: 36950
diff changeset
   337
val opt_newline = Scan.option (Scan.one Token.is_newline);
22124
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
   338
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
   339
val ignore =
36959
f5417836dbea renamed structure OuterLex to Token and type token to Token.T, keeping legacy aliases for some time;
wenzelm
parents: 36950
diff changeset
   340
  Scan.depend (fn d => opt_newline |-- Scan.one Token.is_begin_ignore
22124
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
   341
    >> pair (d + 1)) ||
36959
f5417836dbea renamed structure OuterLex to Token and type token to Token.T, keeping legacy aliases for some time;
wenzelm
parents: 36950
diff changeset
   342
  Scan.depend (fn d => Scan.one Token.is_end_ignore --|
43947
9b00f09f7721 defer evaluation of Scan.message, for improved performance in the frequent situation where failure is handled later (e.g. via ||);
wenzelm
parents: 43564
diff changeset
   343
    (if d = 0 then Scan.fail_with (K (fn () => "Bad nesting of meta-comments")) else opt_newline)
22124
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
   344
    >> pair (d - 1));
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
   345
36950
75b8f26f2f07 refer directly to structure Keyword and Parse;
wenzelm
parents: 36745
diff changeset
   346
val tag = (improper -- Parse.$$$ "%" -- improper) |-- Parse.!!! (Parse.tag_name --| blank_end);
22124
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
   347
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
   348
val locale =
36950
75b8f26f2f07 refer directly to structure Keyword and Parse;
wenzelm
parents: 36745
diff changeset
   349
  Scan.option ((Parse.$$$ "(" -- improper -- Parse.$$$ "in") |--
75b8f26f2f07 refer directly to structure Keyword and Parse;
wenzelm
parents: 36745
diff changeset
   350
    Parse.!!! (improper |-- Parse.xname --| (improper -- Parse.$$$ ")")));
22124
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
   351
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
   352
in
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
   353
46811
03a2dc9e0624 clarified command span: include trailing whitespace/comments and thus reduce number of ignored spans with associated transactions and states (factor 2);
wenzelm
parents: 46261
diff changeset
   354
fun present_thy lex default_tags is_markup command_results toks =
22124
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
   355
  let
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
   356
    (* tokens *)
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
   357
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
   358
    val ignored = Scan.state --| ignore
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
   359
      >> (fn d => (NONE, (NoToken, ("", d))));
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
   360
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
   361
    fun markup mark mk flag = Scan.peek (fn d =>
36950
75b8f26f2f07 refer directly to structure Keyword and Parse;
wenzelm
parents: 36745
diff changeset
   362
      improper |--
46811
03a2dc9e0624 clarified command span: include trailing whitespace/comments and thus reduce number of ignored spans with associated transactions and states (factor 2);
wenzelm
parents: 46261
diff changeset
   363
        Parse.position (Scan.one (Token.is_command andf is_markup mark o Token.content_of)) --
22124
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
   364
      Scan.repeat tag --
51627
589daaf48dba tuned signature -- agree with markup terminology;
wenzelm
parents: 51626
diff changeset
   365
      Parse.!!!! ((improper -- locale -- improper) |-- Parse.document_source --| improper_end)
22124
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
   366
      >> (fn (((tok, pos), tags), txt) =>
36959
f5417836dbea renamed structure OuterLex to Token and type token to Token.T, keeping legacy aliases for some time;
wenzelm
parents: 36950
diff changeset
   367
        let val name = Token.content_of tok
22124
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
   368
        in (SOME (name, pos, tags), (mk (name, txt), (flag, d))) end));
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
   369
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
   370
    val command = Scan.peek (fn d =>
46811
03a2dc9e0624 clarified command span: include trailing whitespace/comments and thus reduce number of ignored spans with associated transactions and states (factor 2);
wenzelm
parents: 46261
diff changeset
   371
      Parse.position (Scan.one (Token.is_command)) --
22124
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
   372
      Scan.repeat tag
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
   373
      >> (fn ((tok, pos), tags) =>
36959
f5417836dbea renamed structure OuterLex to Token and type token to Token.T, keeping legacy aliases for some time;
wenzelm
parents: 36950
diff changeset
   374
        let val name = Token.content_of tok
22124
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
   375
        in (SOME (name, pos, tags), (BasicToken tok, (Latex.markup_false, d))) end));
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
   376
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
   377
    val cmt = Scan.peek (fn d =>
51627
589daaf48dba tuned signature -- agree with markup terminology;
wenzelm
parents: 51626
diff changeset
   378
      Parse.$$$ "--" |-- Parse.!!!! (improper |-- Parse.document_source)
22124
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
   379
      >> (fn txt => (NONE, (MarkupToken ("cmt", txt), ("", d)))));
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
   380
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
   381
    val other = Scan.peek (fn d =>
36950
75b8f26f2f07 refer directly to structure Keyword and Parse;
wenzelm
parents: 36745
diff changeset
   382
       Parse.not_eof >> (fn tok => (NONE, (BasicToken tok, ("", d)))));
22124
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
   383
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
   384
    val token =
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
   385
      ignored ||
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
   386
      markup Markup MarkupToken Latex.markup_true ||
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
   387
      markup MarkupEnv MarkupEnvToken Latex.markup_true ||
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
   388
      markup Verbatim (VerbatimToken o #2) "" ||
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
   389
      command || cmt || other;
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
   390
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
   391
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
   392
    (* spans *)
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
   393
36959
f5417836dbea renamed structure OuterLex to Token and type token to Token.T, keeping legacy aliases for some time;
wenzelm
parents: 36950
diff changeset
   394
    val is_eof = fn (_, (BasicToken x, _)) => Token.is_eof x | _ => false;
f5417836dbea renamed structure OuterLex to Token and type token to Token.T, keeping legacy aliases for some time;
wenzelm
parents: 36950
diff changeset
   395
    val stopper = Scan.stopper (K (NONE, (BasicToken Token.eof, ("", 0)))) is_eof;
22124
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
   396
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
   397
    val cmd = Scan.one (is_some o fst);
27732
8dbf5761a24a abstract type Scan.stopper;
wenzelm
parents: 27566
diff changeset
   398
    val non_cmd = Scan.one (is_none o fst andf not o is_eof) >> #2;
22124
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
   399
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
   400
    val comments = Scan.many (comment_token o fst o snd);
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
   401
    val blank = Scan.one (blank_token o fst o snd);
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
   402
    val newline = Scan.one (newline_token o fst o snd);
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
   403
    val before_cmd =
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
   404
      Scan.option (newline -- comments) --
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
   405
      Scan.option (newline -- comments) --
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
   406
      Scan.option (blank -- comments) -- cmd;
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
   407
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
   408
    val span =
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
   409
      Scan.repeat non_cmd -- cmd --
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
   410
        Scan.repeat (Scan.unless before_cmd non_cmd) --
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
   411
        Scan.option (newline >> (single o snd))
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
   412
      >> (fn (((toks1, (cmd, tok2)), toks3), tok4) =>
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
   413
          make_span (the cmd) (toks1 @ (tok2 :: (toks3 @ the_default [] tok4))));
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
   414
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
   415
    val spans =
46811
03a2dc9e0624 clarified command span: include trailing whitespace/comments and thus reduce number of ignored spans with associated transactions and states (factor 2);
wenzelm
parents: 46261
diff changeset
   416
      Source.of_list (filter_out Token.is_semicolon toks)
36959
f5417836dbea renamed structure OuterLex to Token and type token to Token.T, keeping legacy aliases for some time;
wenzelm
parents: 36950
diff changeset
   417
      |> Source.source' 0 Token.stopper (Scan.error (Scan.bulk token)) NONE
22124
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
   418
      |> Source.source stopper (Scan.error (Scan.bulk span)) NONE
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
   419
      |> Source.exhaust;
28427
cc9f7d99fb73 turned process_thy into present_thy, which merely does presentation (wrt. persistent intermediate states);
wenzelm
parents: 28273
diff changeset
   420
cc9f7d99fb73 turned process_thy into present_thy, which merely does presentation (wrt. persistent intermediate states);
wenzelm
parents: 28273
diff changeset
   421
cc9f7d99fb73 turned process_thy into present_thy, which merely does presentation (wrt. persistent intermediate states);
wenzelm
parents: 28273
diff changeset
   422
    (* present commands *)
cc9f7d99fb73 turned process_thy into present_thy, which merely does presentation (wrt. persistent intermediate states);
wenzelm
parents: 28273
diff changeset
   423
cc9f7d99fb73 turned process_thy into present_thy, which merely does presentation (wrt. persistent intermediate states);
wenzelm
parents: 28273
diff changeset
   424
    fun present_command tr span st st' =
cc9f7d99fb73 turned process_thy into present_thy, which merely does presentation (wrt. persistent intermediate states);
wenzelm
parents: 28273
diff changeset
   425
      Toplevel.setmp_thread_position tr (present_span lex default_tags span st st');
cc9f7d99fb73 turned process_thy into present_thy, which merely does presentation (wrt. persistent intermediate states);
wenzelm
parents: 28273
diff changeset
   426
cc9f7d99fb73 turned process_thy into present_thy, which merely does presentation (wrt. persistent intermediate states);
wenzelm
parents: 28273
diff changeset
   427
    fun present _ [] = I
cc9f7d99fb73 turned process_thy into present_thy, which merely does presentation (wrt. persistent intermediate states);
wenzelm
parents: 28273
diff changeset
   428
      | present st (((tr, st'), span) :: rest) = present_command tr span st st' #> present st' rest;
22124
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
   429
  in
28427
cc9f7d99fb73 turned process_thy into present_thy, which merely does presentation (wrt. persistent intermediate states);
wenzelm
parents: 28273
diff changeset
   430
    if length command_results = length spans then
22124
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
   431
      ((NONE, []), NONE, true, Buffer.empty, (I, I))
28427
cc9f7d99fb73 turned process_thy into present_thy, which merely does presentation (wrt. persistent intermediate states);
wenzelm
parents: 28273
diff changeset
   432
      |> present Toplevel.toplevel (command_results ~~ spans)
22124
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
   433
      |> present_trailer
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
   434
    else error "Messed-up outer syntax for presentation"
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
   435
  end;
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
   436
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
   437
end;
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
   438
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
   439
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
   440
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
   441
(** setup default output **)
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
   442
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
   443
(* options *)
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
   444
53171
a5e54d4d9081 added Theory.setup convenience;
wenzelm
parents: 53167
diff changeset
   445
val _ = Theory.setup
a5e54d4d9081 added Theory.setup convenience;
wenzelm
parents: 53167
diff changeset
   446
 (add_option (Binding.name "show_types") (Config.put show_types o boolean) #>
a5e54d4d9081 added Theory.setup convenience;
wenzelm
parents: 53167
diff changeset
   447
  add_option (Binding.name "show_sorts") (Config.put show_sorts o boolean) #>
a5e54d4d9081 added Theory.setup convenience;
wenzelm
parents: 53167
diff changeset
   448
  add_option (Binding.name "show_structs") (Config.put show_structs o boolean) #>
a5e54d4d9081 added Theory.setup convenience;
wenzelm
parents: 53167
diff changeset
   449
  add_option (Binding.name "show_question_marks") (Config.put show_question_marks o boolean) #>
a5e54d4d9081 added Theory.setup convenience;
wenzelm
parents: 53167
diff changeset
   450
  add_option (Binding.name "show_abbrevs") (Config.put show_abbrevs o boolean) #>
a5e54d4d9081 added Theory.setup convenience;
wenzelm
parents: 53167
diff changeset
   451
  add_option (Binding.name "names_long") (Config.put Name_Space.names_long o boolean) #>
a5e54d4d9081 added Theory.setup convenience;
wenzelm
parents: 53167
diff changeset
   452
  add_option (Binding.name "names_short") (Config.put Name_Space.names_short o boolean) #>
a5e54d4d9081 added Theory.setup convenience;
wenzelm
parents: 53167
diff changeset
   453
  add_option (Binding.name "names_unique") (Config.put Name_Space.names_unique o boolean) #>
a5e54d4d9081 added Theory.setup convenience;
wenzelm
parents: 53167
diff changeset
   454
  add_option (Binding.name "eta_contract") (Config.put Syntax_Trans.eta_contract o boolean) #>
a5e54d4d9081 added Theory.setup convenience;
wenzelm
parents: 53167
diff changeset
   455
  add_option (Binding.name "display") (Config.put display o boolean) #>
a5e54d4d9081 added Theory.setup convenience;
wenzelm
parents: 53167
diff changeset
   456
  add_option (Binding.name "break") (Config.put break o boolean) #>
a5e54d4d9081 added Theory.setup convenience;
wenzelm
parents: 53167
diff changeset
   457
  add_option (Binding.name "quotes") (Config.put quotes o boolean) #>
a5e54d4d9081 added Theory.setup convenience;
wenzelm
parents: 53167
diff changeset
   458
  add_option (Binding.name "mode") (add_wrapper o Print_Mode.with_modes o single) #>
a5e54d4d9081 added Theory.setup convenience;
wenzelm
parents: 53167
diff changeset
   459
  add_option (Binding.name "margin") (add_wrapper o setmp_CRITICAL Pretty.margin_default o integer) #>
a5e54d4d9081 added Theory.setup convenience;
wenzelm
parents: 53167
diff changeset
   460
  add_option (Binding.name "indent") (Config.put indent o integer) #>
a5e54d4d9081 added Theory.setup convenience;
wenzelm
parents: 53167
diff changeset
   461
  add_option (Binding.name "source") (Config.put source o boolean) #>
a5e54d4d9081 added Theory.setup convenience;
wenzelm
parents: 53167
diff changeset
   462
  add_option (Binding.name "goals_limit") (Config.put Goal_Display.goals_limit o integer));
22124
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
   463
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
   464
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
   465
(* basic pretty printing *)
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
   466
38767
d8da44a8dd25 proper context for various Thy_Output options, via official configuration options in ML and Isar;
wenzelm
parents: 38766
diff changeset
   467
fun tweak_line ctxt s =
d8da44a8dd25 proper context for various Thy_Output options, via official configuration options in ML and Isar;
wenzelm
parents: 38766
diff changeset
   468
  if Config.get ctxt display then s else Symbol.strip_blanks s;
22124
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
   469
38767
d8da44a8dd25 proper context for various Thy_Output options, via official configuration options in ML and Isar;
wenzelm
parents: 38766
diff changeset
   470
fun pretty_text ctxt =
46195
wenzelm
parents: 45666
diff changeset
   471
  Pretty.chunks o map Pretty.str o map (tweak_line ctxt) o split_lines;
22124
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
   472
55561
88c40aff747d more markup;
wenzelm
parents: 55550
diff changeset
   473
fun pretty_text_report ctxt (s, pos) =
88c40aff747d more markup;
wenzelm
parents: 55550
diff changeset
   474
  (Context_Position.report ctxt pos Markup.language_text; pretty_text ctxt s);
88c40aff747d more markup;
wenzelm
parents: 55550
diff changeset
   475
26710
f79aa228c582 pretty_term: no revert_skolems here, but auto_fixes (token translations will do the rest);
wenzelm
parents: 26455
diff changeset
   476
fun pretty_term ctxt t = Syntax.pretty_term (Variable.auto_fixes t ctxt) t;
24920
2a45e400fdad generic Syntax.pretty/string_of operations;
wenzelm
parents: 24680
diff changeset
   477
32898
e871d897969c term styles also cover antiquotations term_type and typeof
haftmann
parents: 32890
diff changeset
   478
fun pretty_thm ctxt = pretty_term ctxt o Thm.full_prop_of;
e871d897969c term styles also cover antiquotations term_type and typeof
haftmann
parents: 32890
diff changeset
   479
e871d897969c term styles also cover antiquotations term_type and typeof
haftmann
parents: 32890
diff changeset
   480
fun pretty_term_style ctxt (style, t) =
e871d897969c term styles also cover antiquotations term_type and typeof
haftmann
parents: 32890
diff changeset
   481
  pretty_term ctxt (style t);
22124
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
   482
32898
e871d897969c term styles also cover antiquotations term_type and typeof
haftmann
parents: 32890
diff changeset
   483
fun pretty_thm_style ctxt (style, th) =
e871d897969c term styles also cover antiquotations term_type and typeof
haftmann
parents: 32890
diff changeset
   484
  pretty_term ctxt (style (Thm.full_prop_of th));
22124
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
   485
32898
e871d897969c term styles also cover antiquotations term_type and typeof
haftmann
parents: 32890
diff changeset
   486
fun pretty_term_typ ctxt (style, t) =
e871d897969c term styles also cover antiquotations term_type and typeof
haftmann
parents: 32890
diff changeset
   487
  let val t' = style t
39288
f1ae2493d93f eliminated aliases of Type.constraint;
wenzelm
parents: 39134
diff changeset
   488
  in pretty_term ctxt (Type.constraint (Term.fastype_of t') t') end;
32898
e871d897969c term styles also cover antiquotations term_type and typeof
haftmann
parents: 32890
diff changeset
   489
e871d897969c term styles also cover antiquotations term_type and typeof
haftmann
parents: 32890
diff changeset
   490
fun pretty_term_typeof ctxt (style, t) =
e871d897969c term styles also cover antiquotations term_type and typeof
haftmann
parents: 32890
diff changeset
   491
  Syntax.pretty_typ ctxt (Term.fastype_of (style t));
22124
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
   492
25373
ccbf65080fdf @{const}: improved ProofContext.read_const does the job;
wenzelm
parents: 25241
diff changeset
   493
fun pretty_const ctxt c =
ccbf65080fdf @{const}: improved ProofContext.read_const does the job;
wenzelm
parents: 25241
diff changeset
   494
  let
42360
da8817d01e7c modernized structure Proof_Context;
wenzelm
parents: 42359
diff changeset
   495
    val t = Const (c, Consts.type_scheme (Proof_Context.consts_of ctxt) c)
25373
ccbf65080fdf @{const}: improved ProofContext.read_const does the job;
wenzelm
parents: 25241
diff changeset
   496
      handle TYPE (msg, _, _) => error msg;
ccbf65080fdf @{const}: improved ProofContext.read_const does the job;
wenzelm
parents: 25241
diff changeset
   497
    val ([t'], _) = Variable.import_terms true [t] ctxt;
ccbf65080fdf @{const}: improved ProofContext.read_const does the job;
wenzelm
parents: 25241
diff changeset
   498
  in pretty_term ctxt t' end;
22124
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
   499
25407
2859cf34aaf0 abbrev: bypass full term check via ProofContext.standard_infer_types (prevents forced expansion);
wenzelm
parents: 25373
diff changeset
   500
fun pretty_abbrev ctxt s =
22124
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
   501
  let
42399
95b17b4901b5 pretty_abbrev: read abbreviation more directly;
wenzelm
parents: 42360
diff changeset
   502
    val t = Syntax.read_term (Proof_Context.set_mode Proof_Context.mode_abbrev ctxt) s;
24920
2a45e400fdad generic Syntax.pretty/string_of operations;
wenzelm
parents: 24680
diff changeset
   503
    fun err () = error ("Abbreviated constant expected: " ^ Syntax.string_of_term ctxt t);
22124
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
   504
    val (head, args) = Term.strip_comb t;
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
   505
    val (c, T) = Term.dest_Const head handle TERM _ => err ();
42360
da8817d01e7c modernized structure Proof_Context;
wenzelm
parents: 42359
diff changeset
   506
    val (U, u) = Consts.the_abbreviation (Proof_Context.consts_of ctxt) c
22124
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
   507
      handle TYPE _ => err ();
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
   508
    val t' = Term.betapplys (Envir.expand_atom T (U, u), args);
32898
e871d897969c term styles also cover antiquotations term_type and typeof
haftmann
parents: 32890
diff changeset
   509
    val eq = Logic.mk_equals (t, t');
e871d897969c term styles also cover antiquotations term_type and typeof
haftmann
parents: 32890
diff changeset
   510
    val ctxt' = Variable.auto_fixes eq ctxt;
42360
da8817d01e7c modernized structure Proof_Context;
wenzelm
parents: 42359
diff changeset
   511
  in Proof_Context.pretty_term_abbrev ctxt' eq end;
22124
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
   512
39305
d4fa19eb0822 'class' and 'type' are now antiquoations by default
haftmann
parents: 39134
diff changeset
   513
fun pretty_class ctxt =
42360
da8817d01e7c modernized structure Proof_Context;
wenzelm
parents: 42359
diff changeset
   514
  Pretty.str o Proof_Context.extern_class ctxt o Proof_Context.read_class ctxt;
39305
d4fa19eb0822 'class' and 'type' are now antiquoations by default
haftmann
parents: 39134
diff changeset
   515
39309
74469faa27ca type antiquotation: allow arbitrary type abbreviations, but fail with user-space exception on bad input
haftmann
parents: 39308
diff changeset
   516
fun pretty_type ctxt s =
42360
da8817d01e7c modernized structure Proof_Context;
wenzelm
parents: 42359
diff changeset
   517
  let val Type (name, _) = Proof_Context.read_type_name_proper ctxt false s
da8817d01e7c modernized structure Proof_Context;
wenzelm
parents: 42359
diff changeset
   518
  in Pretty.str (Proof_Context.extern_type ctxt name) end;
39305
d4fa19eb0822 'class' and 'type' are now antiquoations by default
haftmann
parents: 39134
diff changeset
   519
33388
d64545e6cba5 modernized structure Proof_Syntax;
wenzelm
parents: 33095
diff changeset
   520
fun pretty_prf full ctxt = Proof_Syntax.pretty_proof_of ctxt full;
22124
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
   521
48927
ef462b5558eb theory def/ref position reports, which enable hyperlinks etc.;
wenzelm
parents: 48918
diff changeset
   522
fun pretty_theory ctxt (name, pos) =
ef462b5558eb theory def/ref position reports, which enable hyperlinks etc.;
wenzelm
parents: 48918
diff changeset
   523
  (case find_first (fn thy => Context.theory_name thy = name)
ef462b5558eb theory def/ref position reports, which enable hyperlinks etc.;
wenzelm
parents: 48918
diff changeset
   524
      (Theory.nodes_of (Proof_Context.theory_of ctxt)) of
48992
0518bf89c777 renamed Position.str_of to Position.here;
wenzelm
parents: 48927
diff changeset
   525
    NONE => error ("No ancestor theory " ^ quote name ^ Position.here pos)
55614
e2d71b8b0d95 prefer guarded Context_Position.report where feasible;
wenzelm
parents: 55561
diff changeset
   526
  | SOME thy => (Context_Position.report ctxt pos (Theory.get_markup thy); Pretty.str name));
22124
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
   527
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
   528
30390
ad591ee76c78 simplified interface to define document antiquotations, cf. antiquotatation, maybe_pretty_source, output;
wenzelm
parents: 30381
diff changeset
   529
(* default output *)
ad591ee76c78 simplified interface to define document antiquotations, cf. antiquotatation, maybe_pretty_source, output;
wenzelm
parents: 30381
diff changeset
   530
36959
f5417836dbea renamed structure OuterLex to Token and type token to Token.T, keeping legacy aliases for some time;
wenzelm
parents: 36950
diff changeset
   531
val str_of_source = space_implode " " o map Token.unparse o #2 o #1 o Args.dest_src;
22124
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
   532
38767
d8da44a8dd25 proper context for various Thy_Output options, via official configuration options in ML and Isar;
wenzelm
parents: 38766
diff changeset
   533
fun maybe_pretty_source pretty ctxt src xs =
d8da44a8dd25 proper context for various Thy_Output options, via official configuration options in ML and Isar;
wenzelm
parents: 38766
diff changeset
   534
  map (pretty ctxt) xs  (*always pretty in order to exhibit errors!*)
d8da44a8dd25 proper context for various Thy_Output options, via official configuration options in ML and Isar;
wenzelm
parents: 38766
diff changeset
   535
  |> (if Config.get ctxt source then K [pretty_text ctxt (str_of_source src)] else I);
30390
ad591ee76c78 simplified interface to define document antiquotations, cf. antiquotatation, maybe_pretty_source, output;
wenzelm
parents: 30381
diff changeset
   536
38767
d8da44a8dd25 proper context for various Thy_Output options, via official configuration options in ML and Isar;
wenzelm
parents: 38766
diff changeset
   537
fun output ctxt prts =
30390
ad591ee76c78 simplified interface to define document antiquotations, cf. antiquotatation, maybe_pretty_source, output;
wenzelm
parents: 30381
diff changeset
   538
  prts
38767
d8da44a8dd25 proper context for various Thy_Output options, via official configuration options in ML and Isar;
wenzelm
parents: 38766
diff changeset
   539
  |> (if Config.get ctxt quotes then map Pretty.quote else I)
d8da44a8dd25 proper context for various Thy_Output options, via official configuration options in ML and Isar;
wenzelm
parents: 38766
diff changeset
   540
  |> (if Config.get ctxt display then
d8da44a8dd25 proper context for various Thy_Output options, via official configuration options in ML and Isar;
wenzelm
parents: 38766
diff changeset
   541
    map (Output.output o Pretty.string_of o Pretty.indent (Config.get ctxt indent))
22124
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
   542
    #> space_implode "\\isasep\\isanewline%\n"
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
   543
    #> enclose "\\begin{isabelle}%\n" "%\n\\end{isabelle}"
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
   544
  else
38767
d8da44a8dd25 proper context for various Thy_Output options, via official configuration options in ML and Isar;
wenzelm
parents: 38766
diff changeset
   545
    map (Output.output o (if Config.get ctxt break then Pretty.string_of else Pretty.str_of))
22124
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
   546
    #> space_implode "\\isasep\\isanewline%\n"
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
   547
    #> enclose "\\isa{" "}");
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
   548
30390
ad591ee76c78 simplified interface to define document antiquotations, cf. antiquotatation, maybe_pretty_source, output;
wenzelm
parents: 30381
diff changeset
   549
ad591ee76c78 simplified interface to define document antiquotations, cf. antiquotatation, maybe_pretty_source, output;
wenzelm
parents: 30381
diff changeset
   550
ad591ee76c78 simplified interface to define document antiquotations, cf. antiquotatation, maybe_pretty_source, output;
wenzelm
parents: 30381
diff changeset
   551
(** concrete antiquotations **)
ad591ee76c78 simplified interface to define document antiquotations, cf. antiquotatation, maybe_pretty_source, output;
wenzelm
parents: 30381
diff changeset
   552
ad591ee76c78 simplified interface to define document antiquotations, cf. antiquotatation, maybe_pretty_source, output;
wenzelm
parents: 30381
diff changeset
   553
(* basic entities *)
ad591ee76c78 simplified interface to define document antiquotations, cf. antiquotatation, maybe_pretty_source, output;
wenzelm
parents: 30381
diff changeset
   554
ad591ee76c78 simplified interface to define document antiquotations, cf. antiquotatation, maybe_pretty_source, output;
wenzelm
parents: 30381
diff changeset
   555
local
ad591ee76c78 simplified interface to define document antiquotations, cf. antiquotatation, maybe_pretty_source, output;
wenzelm
parents: 30381
diff changeset
   556
ad591ee76c78 simplified interface to define document antiquotations, cf. antiquotatation, maybe_pretty_source, output;
wenzelm
parents: 30381
diff changeset
   557
fun basic_entities name scan pretty = antiquotation name scan
38767
d8da44a8dd25 proper context for various Thy_Output options, via official configuration options in ML and Isar;
wenzelm
parents: 38766
diff changeset
   558
  (fn {source, context, ...} => output context o maybe_pretty_source pretty context source);
30390
ad591ee76c78 simplified interface to define document antiquotations, cf. antiquotatation, maybe_pretty_source, output;
wenzelm
parents: 30381
diff changeset
   559
32890
77df12652210 generalized term styles: transformations may depend on arguments; modernized term_style module; antiquotations thm, prop and term accepting term styles
haftmann
parents: 32738
diff changeset
   560
fun basic_entities_style name scan pretty = antiquotation name scan
77df12652210 generalized term styles: transformations may depend on arguments; modernized term_style module; antiquotations thm, prop and term accepting term styles
haftmann
parents: 32738
diff changeset
   561
  (fn {source, context, ...} => fn (style, xs) =>
38767
d8da44a8dd25 proper context for various Thy_Output options, via official configuration options in ML and Isar;
wenzelm
parents: 38766
diff changeset
   562
    output context
d8da44a8dd25 proper context for various Thy_Output options, via official configuration options in ML and Isar;
wenzelm
parents: 38766
diff changeset
   563
      (maybe_pretty_source (fn ctxt => fn x => pretty ctxt (style, x)) context source xs));
32890
77df12652210 generalized term styles: transformations may depend on arguments; modernized term_style module; antiquotations thm, prop and term accepting term styles
haftmann
parents: 32738
diff changeset
   564
30390
ad591ee76c78 simplified interface to define document antiquotations, cf. antiquotatation, maybe_pretty_source, output;
wenzelm
parents: 30381
diff changeset
   565
fun basic_entity name scan = basic_entities name (scan >> single);
ad591ee76c78 simplified interface to define document antiquotations, cf. antiquotatation, maybe_pretty_source, output;
wenzelm
parents: 30381
diff changeset
   566
ad591ee76c78 simplified interface to define document antiquotations, cf. antiquotatation, maybe_pretty_source, output;
wenzelm
parents: 30381
diff changeset
   567
in
ad591ee76c78 simplified interface to define document antiquotations, cf. antiquotatation, maybe_pretty_source, output;
wenzelm
parents: 30381
diff changeset
   568
53171
a5e54d4d9081 added Theory.setup convenience;
wenzelm
parents: 53167
diff changeset
   569
val _ = Theory.setup
a5e54d4d9081 added Theory.setup convenience;
wenzelm
parents: 53167
diff changeset
   570
 (basic_entities_style (Binding.name "thm") (Term_Style.parse -- Attrib.thms) pretty_thm_style #>
a5e54d4d9081 added Theory.setup convenience;
wenzelm
parents: 53167
diff changeset
   571
  basic_entity (Binding.name "prop") (Term_Style.parse -- Args.prop) pretty_term_style #>
a5e54d4d9081 added Theory.setup convenience;
wenzelm
parents: 53167
diff changeset
   572
  basic_entity (Binding.name "term") (Term_Style.parse -- Args.term) pretty_term_style #>
a5e54d4d9081 added Theory.setup convenience;
wenzelm
parents: 53167
diff changeset
   573
  basic_entity (Binding.name "term_type") (Term_Style.parse -- Args.term) pretty_term_typ #>
a5e54d4d9081 added Theory.setup convenience;
wenzelm
parents: 53167
diff changeset
   574
  basic_entity (Binding.name "typeof") (Term_Style.parse -- Args.term) pretty_term_typeof #>
a5e54d4d9081 added Theory.setup convenience;
wenzelm
parents: 53167
diff changeset
   575
  basic_entity (Binding.name "const") (Args.const_proper false) pretty_const #>
55111
5792f5106c40 tuned signature;
wenzelm
parents: 54702
diff changeset
   576
  basic_entity (Binding.name "abbrev") (Scan.lift Args.name_inner_syntax) pretty_abbrev #>
53171
a5e54d4d9081 added Theory.setup convenience;
wenzelm
parents: 53167
diff changeset
   577
  basic_entity (Binding.name "typ") Args.typ_abbrev Syntax.pretty_typ #>
55111
5792f5106c40 tuned signature;
wenzelm
parents: 54702
diff changeset
   578
  basic_entity (Binding.name "class") (Scan.lift Args.name_inner_syntax) pretty_class #>
53171
a5e54d4d9081 added Theory.setup convenience;
wenzelm
parents: 53167
diff changeset
   579
  basic_entity (Binding.name "type") (Scan.lift Args.name) pretty_type #>
55561
88c40aff747d more markup;
wenzelm
parents: 55550
diff changeset
   580
  basic_entity (Binding.name "text") (Scan.lift (Parse.position Args.name)) pretty_text_report #>
53171
a5e54d4d9081 added Theory.setup convenience;
wenzelm
parents: 53167
diff changeset
   581
  basic_entities (Binding.name "prf") Attrib.thms (pretty_prf false) #>
a5e54d4d9081 added Theory.setup convenience;
wenzelm
parents: 53167
diff changeset
   582
  basic_entities (Binding.name "full_prf") Attrib.thms (pretty_prf true) #>
a5e54d4d9081 added Theory.setup convenience;
wenzelm
parents: 53167
diff changeset
   583
  basic_entity (Binding.name "theory") (Scan.lift (Parse.position Args.name)) pretty_theory);
32898
e871d897969c term styles also cover antiquotations term_type and typeof
haftmann
parents: 32890
diff changeset
   584
30390
ad591ee76c78 simplified interface to define document antiquotations, cf. antiquotatation, maybe_pretty_source, output;
wenzelm
parents: 30381
diff changeset
   585
end;
ad591ee76c78 simplified interface to define document antiquotations, cf. antiquotatation, maybe_pretty_source, output;
wenzelm
parents: 30381
diff changeset
   586
ad591ee76c78 simplified interface to define document antiquotations, cf. antiquotatation, maybe_pretty_source, output;
wenzelm
parents: 30381
diff changeset
   587
ad591ee76c78 simplified interface to define document antiquotations, cf. antiquotatation, maybe_pretty_source, output;
wenzelm
parents: 30381
diff changeset
   588
(* goal state *)
ad591ee76c78 simplified interface to define document antiquotations, cf. antiquotatation, maybe_pretty_source, output;
wenzelm
parents: 30381
diff changeset
   589
ad591ee76c78 simplified interface to define document antiquotations, cf. antiquotatation, maybe_pretty_source, output;
wenzelm
parents: 30381
diff changeset
   590
local
22124
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
   591
30367
ee8841b1b981 simplified presentation: pass state directly;
wenzelm
parents: 30317
diff changeset
   592
fun proof_state state =
49847
ed5080c03165 some attempts to unify/simplify pretty_goal;
wenzelm
parents: 49321
diff changeset
   593
  (case try (Proof.goal o Toplevel.proof_of) state of
ed5080c03165 some attempts to unify/simplify pretty_goal;
wenzelm
parents: 49321
diff changeset
   594
    SOME {goal, ...} => goal
22124
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
   595
  | _ => error "No proof state");
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
   596
49847
ed5080c03165 some attempts to unify/simplify pretty_goal;
wenzelm
parents: 49321
diff changeset
   597
fun goal_state name main = antiquotation name (Scan.succeed ())
39125
f45d332a90e3 pretty_goals: turned some global references and function arguments into configuration options (goals_limit = 10, goals_total = true, show_main_goal = false) depending on the context;
wenzelm
parents: 38980
diff changeset
   598
  (fn {state, context = ctxt, ...} => fn () => output ctxt
51958
bca32217b304 retain goal display options when printing error messages, to avoid breakdown for huge goals;
wenzelm
parents: 51627
diff changeset
   599
    [Goal_Display.pretty_goal
bca32217b304 retain goal display options when printing error messages, to avoid breakdown for huge goals;
wenzelm
parents: 51627
diff changeset
   600
      (Config.put Goal_Display.show_main_goal main ctxt) (proof_state state)]);
22124
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
   601
30390
ad591ee76c78 simplified interface to define document antiquotations, cf. antiquotatation, maybe_pretty_source, output;
wenzelm
parents: 30381
diff changeset
   602
in
ad591ee76c78 simplified interface to define document antiquotations, cf. antiquotatation, maybe_pretty_source, output;
wenzelm
parents: 30381
diff changeset
   603
53171
a5e54d4d9081 added Theory.setup convenience;
wenzelm
parents: 53167
diff changeset
   604
val _ = Theory.setup
a5e54d4d9081 added Theory.setup convenience;
wenzelm
parents: 53167
diff changeset
   605
 (goal_state (Binding.name "goals") true #>
a5e54d4d9081 added Theory.setup convenience;
wenzelm
parents: 53167
diff changeset
   606
  goal_state (Binding.name "subgoals") false);
30390
ad591ee76c78 simplified interface to define document antiquotations, cf. antiquotatation, maybe_pretty_source, output;
wenzelm
parents: 30381
diff changeset
   607
ad591ee76c78 simplified interface to define document antiquotations, cf. antiquotatation, maybe_pretty_source, output;
wenzelm
parents: 30381
diff changeset
   608
end;
22124
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
   609
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
   610
30390
ad591ee76c78 simplified interface to define document antiquotations, cf. antiquotatation, maybe_pretty_source, output;
wenzelm
parents: 30381
diff changeset
   611
(* embedded lemma *)
27522
b819d3b263a0 @{lemma}: allow terminal method;
wenzelm
parents: 27381
diff changeset
   612
46958
0ec8f04e753a define keywords early when processing the theory header, before running the body commands;
wenzelm
parents: 46957
diff changeset
   613
val _ = Keyword.define ("by", NONE);  (*overlap with command category*)
46950
d0181abdbdac declare command keywords via theory header, including strict checking outside Pure;
wenzelm
parents: 46947
diff changeset
   614
53171
a5e54d4d9081 added Theory.setup convenience;
wenzelm
parents: 53167
diff changeset
   615
val _ = Theory.setup
a5e54d4d9081 added Theory.setup convenience;
wenzelm
parents: 53167
diff changeset
   616
  (antiquotation (Binding.name "lemma")
55739
d8270c17b5be more markup;
wenzelm
parents: 55614
diff changeset
   617
    (Args.prop --
d8270c17b5be more markup;
wenzelm
parents: 55614
diff changeset
   618
      Scan.lift (Parse.position (Args.$$$ "by") -- (Method.parse -- Scan.option Method.parse)))
d8270c17b5be more markup;
wenzelm
parents: 55614
diff changeset
   619
    (fn {source, context = ctxt, ...} => fn (prop, ((_, by_pos), methods)) =>
43564
9864182c6bad document antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents: 42669
diff changeset
   620
      let
9864182c6bad document antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents: 42669
diff changeset
   621
        val prop_src =
9864182c6bad document antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents: 42669
diff changeset
   622
          (case Args.dest_src source of ((a, arg :: _), pos) => Args.src ((a, [arg]), pos));
55739
d8270c17b5be more markup;
wenzelm
parents: 55614
diff changeset
   623
        val _ = Context_Position.report ctxt by_pos Markup.keyword1;
43564
9864182c6bad document antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents: 42669
diff changeset
   624
        (* FIXME check proof!? *)
55739
d8270c17b5be more markup;
wenzelm
parents: 55614
diff changeset
   625
        val _ = ctxt
43564
9864182c6bad document antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents: 42669
diff changeset
   626
          |> Proof.theorem NONE (K I) [[(prop, [])]]
9864182c6bad document antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents: 42669
diff changeset
   627
          |> Proof.global_terminal_proof methods;
55739
d8270c17b5be more markup;
wenzelm
parents: 55614
diff changeset
   628
      in output ctxt (maybe_pretty_source pretty_term ctxt prop_src [prop]) end));
30390
ad591ee76c78 simplified interface to define document antiquotations, cf. antiquotatation, maybe_pretty_source, output;
wenzelm
parents: 30381
diff changeset
   629
ad591ee76c78 simplified interface to define document antiquotations, cf. antiquotatation, maybe_pretty_source, output;
wenzelm
parents: 30381
diff changeset
   630
ad591ee76c78 simplified interface to define document antiquotations, cf. antiquotatation, maybe_pretty_source, output;
wenzelm
parents: 30381
diff changeset
   631
(* ML text *)
ad591ee76c78 simplified interface to define document antiquotations, cf. antiquotatation, maybe_pretty_source, output;
wenzelm
parents: 30381
diff changeset
   632
40801
6cfacec435e6 added document antiquotation @{file};
wenzelm
parents: 40800
diff changeset
   633
val verb_text =
6cfacec435e6 added document antiquotation @{file};
wenzelm
parents: 40800
diff changeset
   634
  split_lines
6cfacec435e6 added document antiquotation @{file};
wenzelm
parents: 40800
diff changeset
   635
  #> map (space_implode "\\verb,|," o map (enclose "\\verb|" "|") o space_explode "|")
6cfacec435e6 added document antiquotation @{file};
wenzelm
parents: 40800
diff changeset
   636
  #> space_implode "\\isasep\\isanewline%\n";
6cfacec435e6 added document antiquotation @{file};
wenzelm
parents: 40800
diff changeset
   637
30390
ad591ee76c78 simplified interface to define document antiquotations, cf. antiquotatation, maybe_pretty_source, output;
wenzelm
parents: 30381
diff changeset
   638
local
ad591ee76c78 simplified interface to define document antiquotations, cf. antiquotatation, maybe_pretty_source, output;
wenzelm
parents: 30381
diff changeset
   639
ad591ee76c78 simplified interface to define document antiquotations, cf. antiquotatation, maybe_pretty_source, output;
wenzelm
parents: 30381
diff changeset
   640
fun ml_text name ml = antiquotation name (Scan.lift Args.name_source_position)
ad591ee76c78 simplified interface to define document antiquotations, cf. antiquotatation, maybe_pretty_source, output;
wenzelm
parents: 30381
diff changeset
   641
  (fn {context, ...} => fn (txt, pos) =>
37198
3af985b10550 replaced ML_Lex.read_antiq by more concise ML_Lex.read, which includes full read/report with explicit position information;
wenzelm
parents: 37146
diff changeset
   642
   (ML_Context.eval_in (SOME context) false pos (ml pos txt);
30573
49899f26fbd1 de-camelized Symbol_Pos;
wenzelm
parents: 30513
diff changeset
   643
    Symbol_Pos.content (Symbol_Pos.explode (txt, pos))
38767
d8da44a8dd25 proper context for various Thy_Output options, via official configuration options in ML and Isar;
wenzelm
parents: 38766
diff changeset
   644
    |> (if Config.get context quotes then quote else I)
d8da44a8dd25 proper context for various Thy_Output options, via official configuration options in ML and Isar;
wenzelm
parents: 38766
diff changeset
   645
    |> (if Config.get context display then enclose "\\begin{verbatim}\n" "\n\\end{verbatim}"
40801
6cfacec435e6 added document antiquotation @{file};
wenzelm
parents: 40800
diff changeset
   646
        else verb_text)));
30390
ad591ee76c78 simplified interface to define document antiquotations, cf. antiquotatation, maybe_pretty_source, output;
wenzelm
parents: 30381
diff changeset
   647
37198
3af985b10550 replaced ML_Lex.read_antiq by more concise ML_Lex.read, which includes full read/report with explicit position information;
wenzelm
parents: 37146
diff changeset
   648
fun ml_enclose bg en pos txt =
3af985b10550 replaced ML_Lex.read_antiq by more concise ML_Lex.read, which includes full read/report with explicit position information;
wenzelm
parents: 37146
diff changeset
   649
  ML_Lex.read Position.none bg @ ML_Lex.read pos txt @ ML_Lex.read Position.none en;
3af985b10550 replaced ML_Lex.read_antiq by more concise ML_Lex.read, which includes full read/report with explicit position information;
wenzelm
parents: 37146
diff changeset
   650
30390
ad591ee76c78 simplified interface to define document antiquotations, cf. antiquotatation, maybe_pretty_source, output;
wenzelm
parents: 30381
diff changeset
   651
in
ad591ee76c78 simplified interface to define document antiquotations, cf. antiquotatation, maybe_pretty_source, output;
wenzelm
parents: 30381
diff changeset
   652
53171
a5e54d4d9081 added Theory.setup convenience;
wenzelm
parents: 53167
diff changeset
   653
val _ = Theory.setup
a5e54d4d9081 added Theory.setup convenience;
wenzelm
parents: 53167
diff changeset
   654
 (ml_text (Binding.name "ML") (ml_enclose "fn _ => (" ");") #>
a5e54d4d9081 added Theory.setup convenience;
wenzelm
parents: 53167
diff changeset
   655
  ml_text (Binding.name "ML_op") (ml_enclose "fn _ => (op " ");") #>
a5e54d4d9081 added Theory.setup convenience;
wenzelm
parents: 53167
diff changeset
   656
  ml_text (Binding.name "ML_type") (ml_enclose "val _ = NONE : (" ") option;") #>
a5e54d4d9081 added Theory.setup convenience;
wenzelm
parents: 53167
diff changeset
   657
  ml_text (Binding.name "ML_struct")
a5e54d4d9081 added Theory.setup convenience;
wenzelm
parents: 53167
diff changeset
   658
    (ml_enclose "functor XXX() = struct structure XX = " " end;") #>
37198
3af985b10550 replaced ML_Lex.read_antiq by more concise ML_Lex.read, which includes full read/report with explicit position information;
wenzelm
parents: 37146
diff changeset
   659
53171
a5e54d4d9081 added Theory.setup convenience;
wenzelm
parents: 53167
diff changeset
   660
  ml_text (Binding.name "ML_functor")   (* FIXME formal treatment of functor name (!?) *)
a5e54d4d9081 added Theory.setup convenience;
wenzelm
parents: 53167
diff changeset
   661
    (fn pos => fn txt =>
a5e54d4d9081 added Theory.setup convenience;
wenzelm
parents: 53167
diff changeset
   662
      ML_Lex.read Position.none ("ML_Env.check_functor " ^
a5e54d4d9081 added Theory.setup convenience;
wenzelm
parents: 53167
diff changeset
   663
        ML_Syntax.print_string (Symbol_Pos.content (Symbol_Pos.explode (txt, pos))))) #>
37198
3af985b10550 replaced ML_Lex.read_antiq by more concise ML_Lex.read, which includes full read/report with explicit position information;
wenzelm
parents: 37146
diff changeset
   664
53171
a5e54d4d9081 added Theory.setup convenience;
wenzelm
parents: 53167
diff changeset
   665
  ml_text (Binding.name "ML_text") (K (K [])));
22124
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
   666
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
   667
end;
30390
ad591ee76c78 simplified interface to define document antiquotations, cf. antiquotatation, maybe_pretty_source, output;
wenzelm
parents: 30381
diff changeset
   668
54702
3daeba5130f0 added document antiquotation @{url}, which produces formal markup for LaTeX and PIDE;
wenzelm
parents: 53171
diff changeset
   669
3daeba5130f0 added document antiquotation @{url}, which produces formal markup for LaTeX and PIDE;
wenzelm
parents: 53171
diff changeset
   670
(* URLs *)
3daeba5130f0 added document antiquotation @{url}, which produces formal markup for LaTeX and PIDE;
wenzelm
parents: 53171
diff changeset
   671
3daeba5130f0 added document antiquotation @{url}, which produces formal markup for LaTeX and PIDE;
wenzelm
parents: 53171
diff changeset
   672
val _ = Theory.setup
3daeba5130f0 added document antiquotation @{url}, which produces formal markup for LaTeX and PIDE;
wenzelm
parents: 53171
diff changeset
   673
  (antiquotation (Binding.name "url") (Scan.lift (Parse.position Parse.name))
3daeba5130f0 added document antiquotation @{url}, which produces formal markup for LaTeX and PIDE;
wenzelm
parents: 53171
diff changeset
   674
    (fn {context = ctxt, ...} => fn (name, pos) =>
55614
e2d71b8b0d95 prefer guarded Context_Position.report where feasible;
wenzelm
parents: 55561
diff changeset
   675
      (Context_Position.report ctxt pos (Markup.url name); enclose "\\url{" "}" name)));
54702
3daeba5130f0 added document antiquotation @{url}, which produces formal markup for LaTeX and PIDE;
wenzelm
parents: 53171
diff changeset
   676
30390
ad591ee76c78 simplified interface to define document antiquotations, cf. antiquotatation, maybe_pretty_source, output;
wenzelm
parents: 30381
diff changeset
   677
end;