src/Pure/Isar/isar_output.ML
author wenzelm
Fri, 21 May 2004 21:19:18 +0200
changeset 14776 4f3b383a46ae
parent 14707 2d6350d7b9b7
child 14835 695ee8ad0bb6
permissions -rw-r--r--
Args.local_typ_raw;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
9140
69e8938c2409 Isar theory output.
wenzelm
parents:
diff changeset
     1
(*  Title:      Pure/Isar/isar_output.ML
69e8938c2409 Isar theory output.
wenzelm
parents:
diff changeset
     2
    ID:         $Id$
69e8938c2409 Isar theory output.
wenzelm
parents:
diff changeset
     3
    Author:     Markus Wenzel, TU Muenchen
69e8938c2409 Isar theory output.
wenzelm
parents:
diff changeset
     4
    License:    GPL (GNU GENERAL PUBLIC LICENSE)
69e8938c2409 Isar theory output.
wenzelm
parents:
diff changeset
     5
69e8938c2409 Isar theory output.
wenzelm
parents:
diff changeset
     6
Isar theory output.
69e8938c2409 Isar theory output.
wenzelm
parents:
diff changeset
     7
*)
69e8938c2409 Isar theory output.
wenzelm
parents:
diff changeset
     8
69e8938c2409 Isar theory output.
wenzelm
parents:
diff changeset
     9
signature ISAR_OUTPUT =
69e8938c2409 Isar theory output.
wenzelm
parents:
diff changeset
    10
sig
10321
bbaad3045e37 let commands access Toplevel.state;
wenzelm
parents: 9863
diff changeset
    11
  val add_commands: (string * (Args.src -> Toplevel.state -> string)) list -> unit
9140
69e8938c2409 Isar theory output.
wenzelm
parents:
diff changeset
    12
  val add_options: (string * (string -> (unit -> string) -> unit -> string)) list -> unit
9220
d0506ced27c8 added options "eta_contract", "long_names";
wenzelm
parents: 9213
diff changeset
    13
  val print_antiquotations: unit -> unit
9140
69e8938c2409 Isar theory output.
wenzelm
parents:
diff changeset
    14
  val boolean: string -> bool
69e8938c2409 Isar theory output.
wenzelm
parents:
diff changeset
    15
  val integer: string -> int
69e8938c2409 Isar theory output.
wenzelm
parents:
diff changeset
    16
  val args: (Proof.context * Args.T list -> 'a * (Proof.context * Args.T list)) ->
10321
bbaad3045e37 let commands access Toplevel.state;
wenzelm
parents: 9863
diff changeset
    17
    (Args.src -> Proof.context -> 'a -> string) -> Args.src -> Toplevel.state -> string
9140
69e8938c2409 Isar theory output.
wenzelm
parents:
diff changeset
    18
  datatype markup = Markup | MarkupEnv | Verbatim
69e8938c2409 Isar theory output.
wenzelm
parents:
diff changeset
    19
  val interest_level: int ref
11714
bc0a84063a9c added global modes ref;
wenzelm
parents: 11524
diff changeset
    20
  val modes: string list ref
12939
279a3cf23a98 export eval_antiquote;
wenzelm
parents: 12881
diff changeset
    21
  val eval_antiquote: Scan.lexicon -> Toplevel.state -> string * Position.T -> string
9140
69e8938c2409 Isar theory output.
wenzelm
parents:
diff changeset
    22
  val parse_thy: (markup -> OuterLex.token list -> OuterLex.token * OuterLex.token list) ->
69e8938c2409 Isar theory output.
wenzelm
parents:
diff changeset
    23
    Scan.lexicon -> Toplevel.transition list -> (OuterLex.token, 'a) Source.source ->
69e8938c2409 Isar theory output.
wenzelm
parents:
diff changeset
    24
      (Toplevel.transition * (Toplevel.state -> Buffer.T -> Buffer.T)) list * Buffer.T
69e8938c2409 Isar theory output.
wenzelm
parents:
diff changeset
    25
  val display: bool ref
69e8938c2409 Isar theory output.
wenzelm
parents:
diff changeset
    26
  val quotes: bool ref
9732
c32c7ef228c6 added "name" antiq and "indent" option;
wenzelm
parents: 9504
diff changeset
    27
  val indent: int ref
9750
270cd9831e7b added "source" option;
wenzelm
parents: 9732
diff changeset
    28
  val source: bool ref
11716
064833efb479 Exported output_with.
berghofe
parents: 11714
diff changeset
    29
  val output_with: (Proof.context -> 'a -> Pretty.T) -> Args.src ->
064833efb479 Exported output_with.
berghofe
parents: 11714
diff changeset
    30
    Proof.context -> 'a -> string
9140
69e8938c2409 Isar theory output.
wenzelm
parents:
diff changeset
    31
end;
69e8938c2409 Isar theory output.
wenzelm
parents:
diff changeset
    32
69e8938c2409 Isar theory output.
wenzelm
parents:
diff changeset
    33
structure IsarOutput: ISAR_OUTPUT =
69e8938c2409 Isar theory output.
wenzelm
parents:
diff changeset
    34
struct
69e8938c2409 Isar theory output.
wenzelm
parents:
diff changeset
    35
69e8938c2409 Isar theory output.
wenzelm
parents:
diff changeset
    36
structure T = OuterLex;
69e8938c2409 Isar theory output.
wenzelm
parents:
diff changeset
    37
structure P = OuterParse;
69e8938c2409 Isar theory output.
wenzelm
parents:
diff changeset
    38
69e8938c2409 Isar theory output.
wenzelm
parents:
diff changeset
    39
69e8938c2409 Isar theory output.
wenzelm
parents:
diff changeset
    40
(** maintain global commands **)
69e8938c2409 Isar theory output.
wenzelm
parents:
diff changeset
    41
69e8938c2409 Isar theory output.
wenzelm
parents:
diff changeset
    42
local
69e8938c2409 Isar theory output.
wenzelm
parents:
diff changeset
    43
69e8938c2409 Isar theory output.
wenzelm
parents:
diff changeset
    44
val global_commands =
10321
bbaad3045e37 let commands access Toplevel.state;
wenzelm
parents: 9863
diff changeset
    45
  ref (Symtab.empty: (Args.src -> Toplevel.state -> string) Symtab.table);
9140
69e8938c2409 Isar theory output.
wenzelm
parents:
diff changeset
    46
69e8938c2409 Isar theory output.
wenzelm
parents:
diff changeset
    47
val global_options =
69e8938c2409 Isar theory output.
wenzelm
parents:
diff changeset
    48
  ref (Symtab.empty: (string -> (unit -> string) -> unit -> string) Symtab.table);
69e8938c2409 Isar theory output.
wenzelm
parents:
diff changeset
    49
69e8938c2409 Isar theory output.
wenzelm
parents:
diff changeset
    50
69e8938c2409 Isar theory output.
wenzelm
parents:
diff changeset
    51
fun add_item kind (tab, (name, x)) =
69e8938c2409 Isar theory output.
wenzelm
parents:
diff changeset
    52
 (if is_none (Symtab.lookup (tab, name)) then ()
69e8938c2409 Isar theory output.
wenzelm
parents:
diff changeset
    53
  else warning ("Redefined antiquotation output " ^ kind ^ ": " ^ quote name);
69e8938c2409 Isar theory output.
wenzelm
parents:
diff changeset
    54
  Symtab.update ((name, x), tab));
69e8938c2409 Isar theory output.
wenzelm
parents:
diff changeset
    55
69e8938c2409 Isar theory output.
wenzelm
parents:
diff changeset
    56
fun add_items kind xs tab = foldl (add_item kind) (tab, xs);
69e8938c2409 Isar theory output.
wenzelm
parents:
diff changeset
    57
69e8938c2409 Isar theory output.
wenzelm
parents:
diff changeset
    58
in
69e8938c2409 Isar theory output.
wenzelm
parents:
diff changeset
    59
69e8938c2409 Isar theory output.
wenzelm
parents:
diff changeset
    60
val add_commands = Library.change global_commands o (add_items "command");
69e8938c2409 Isar theory output.
wenzelm
parents:
diff changeset
    61
val add_options = Library.change global_options o (add_items "option");
69e8938c2409 Isar theory output.
wenzelm
parents:
diff changeset
    62
69e8938c2409 Isar theory output.
wenzelm
parents:
diff changeset
    63
fun command src =
69e8938c2409 Isar theory output.
wenzelm
parents:
diff changeset
    64
  let val ((name, _), pos) = Args.dest_src src in
69e8938c2409 Isar theory output.
wenzelm
parents:
diff changeset
    65
    (case Symtab.lookup (! global_commands, name) of
69e8938c2409 Isar theory output.
wenzelm
parents:
diff changeset
    66
      None => error ("Unknown antiquotation command: " ^ quote name ^ Position.str_of pos)
12881
eeb36b66480e ANTIQUOTE_FAIL;
wenzelm
parents: 12805
diff changeset
    67
    | Some f => transform_failure (curry Antiquote.ANTIQUOTE_FAIL (name, pos)) (f src))
9140
69e8938c2409 Isar theory output.
wenzelm
parents:
diff changeset
    68
  end;
69e8938c2409 Isar theory output.
wenzelm
parents:
diff changeset
    69
69e8938c2409 Isar theory output.
wenzelm
parents:
diff changeset
    70
fun option (name, s) f () =
69e8938c2409 Isar theory output.
wenzelm
parents:
diff changeset
    71
  (case Symtab.lookup (! global_options, name) of
69e8938c2409 Isar theory output.
wenzelm
parents:
diff changeset
    72
    None => error ("Unknown antiquotation option: " ^ quote name)
69e8938c2409 Isar theory output.
wenzelm
parents:
diff changeset
    73
  | Some opt => opt s f ());
69e8938c2409 Isar theory output.
wenzelm
parents:
diff changeset
    74
69e8938c2409 Isar theory output.
wenzelm
parents:
diff changeset
    75
fun options [] f = f
69e8938c2409 Isar theory output.
wenzelm
parents:
diff changeset
    76
  | options (opt :: opts) f = option opt (options opts f);
69e8938c2409 Isar theory output.
wenzelm
parents:
diff changeset
    77
9213
2651a4db8883 help_antiquotations;
wenzelm
parents: 9140
diff changeset
    78
9220
d0506ced27c8 added options "eta_contract", "long_names";
wenzelm
parents: 9213
diff changeset
    79
fun print_antiquotations () =
d0506ced27c8 added options "eta_contract", "long_names";
wenzelm
parents: 9213
diff changeset
    80
 [Pretty.big_list "antiquotation commands:" (map Pretty.str (Symtab.keys (! global_commands))),
d0506ced27c8 added options "eta_contract", "long_names";
wenzelm
parents: 9213
diff changeset
    81
  Pretty.big_list "antiquotation options:" (map Pretty.str (Symtab.keys (! global_options)))]
d0506ced27c8 added options "eta_contract", "long_names";
wenzelm
parents: 9213
diff changeset
    82
 |> Pretty.chunks |> Pretty.writeln;
9213
2651a4db8883 help_antiquotations;
wenzelm
parents: 9140
diff changeset
    83
9140
69e8938c2409 Isar theory output.
wenzelm
parents:
diff changeset
    84
end;
69e8938c2409 Isar theory output.
wenzelm
parents:
diff changeset
    85
69e8938c2409 Isar theory output.
wenzelm
parents:
diff changeset
    86
69e8938c2409 Isar theory output.
wenzelm
parents:
diff changeset
    87
69e8938c2409 Isar theory output.
wenzelm
parents:
diff changeset
    88
(** syntax of antiquotations **)
69e8938c2409 Isar theory output.
wenzelm
parents:
diff changeset
    89
69e8938c2409 Isar theory output.
wenzelm
parents:
diff changeset
    90
(* option values *)
69e8938c2409 Isar theory output.
wenzelm
parents:
diff changeset
    91
69e8938c2409 Isar theory output.
wenzelm
parents:
diff changeset
    92
fun boolean "" = true
69e8938c2409 Isar theory output.
wenzelm
parents:
diff changeset
    93
  | boolean "true" = true
69e8938c2409 Isar theory output.
wenzelm
parents:
diff changeset
    94
  | boolean "false" = false
69e8938c2409 Isar theory output.
wenzelm
parents:
diff changeset
    95
  | boolean s = error ("Bad boolean value: " ^ quote s);
69e8938c2409 Isar theory output.
wenzelm
parents:
diff changeset
    96
69e8938c2409 Isar theory output.
wenzelm
parents:
diff changeset
    97
fun integer s =
69e8938c2409 Isar theory output.
wenzelm
parents:
diff changeset
    98
  let
69e8938c2409 Isar theory output.
wenzelm
parents:
diff changeset
    99
    fun int ss =
69e8938c2409 Isar theory output.
wenzelm
parents:
diff changeset
   100
      (case Term.read_int ss of (i, []) => i | _ => error ("Bad integer value: " ^ quote s));
69e8938c2409 Isar theory output.
wenzelm
parents:
diff changeset
   101
  in (case Symbol.explode s of "-" :: ss => ~ (int ss) | ss => int ss) end;
69e8938c2409 Isar theory output.
wenzelm
parents:
diff changeset
   102
69e8938c2409 Isar theory output.
wenzelm
parents:
diff changeset
   103
69e8938c2409 Isar theory output.
wenzelm
parents:
diff changeset
   104
(* args syntax *)
69e8938c2409 Isar theory output.
wenzelm
parents:
diff changeset
   105
69e8938c2409 Isar theory output.
wenzelm
parents:
diff changeset
   106
fun syntax (scan: (Proof.context * Args.T list -> 'a * (Proof.context * Args.T list))) =
69e8938c2409 Isar theory output.
wenzelm
parents:
diff changeset
   107
  Args.syntax "antiquotation" scan;
69e8938c2409 Isar theory output.
wenzelm
parents:
diff changeset
   108
10321
bbaad3045e37 let commands access Toplevel.state;
wenzelm
parents: 9863
diff changeset
   109
fun args scan f src state : string =
bbaad3045e37 let commands access Toplevel.state;
wenzelm
parents: 9863
diff changeset
   110
  let val (ctxt, x) = syntax scan src (Toplevel.context_of state)
bbaad3045e37 let commands access Toplevel.state;
wenzelm
parents: 9863
diff changeset
   111
  in f src ctxt x end;
9140
69e8938c2409 Isar theory output.
wenzelm
parents:
diff changeset
   112
69e8938c2409 Isar theory output.
wenzelm
parents:
diff changeset
   113
69e8938c2409 Isar theory output.
wenzelm
parents:
diff changeset
   114
(* outer syntax *)
69e8938c2409 Isar theory output.
wenzelm
parents:
diff changeset
   115
69e8938c2409 Isar theory output.
wenzelm
parents:
diff changeset
   116
local
69e8938c2409 Isar theory output.
wenzelm
parents:
diff changeset
   117
69e8938c2409 Isar theory output.
wenzelm
parents:
diff changeset
   118
val property = P.xname -- Scan.optional (P.$$$ "=" |-- P.!!! P.xname) "";
69e8938c2409 Isar theory output.
wenzelm
parents:
diff changeset
   119
val properties = Scan.optional (P.$$$ "[" |-- P.!!! (P.enum "," property --| P.$$$ "]")) [];
69e8938c2409 Isar theory output.
wenzelm
parents:
diff changeset
   120
69e8938c2409 Isar theory output.
wenzelm
parents:
diff changeset
   121
val antiq = P.position P.xname -- properties -- P.arguments --| Scan.ahead P.eof
69e8938c2409 Isar theory output.
wenzelm
parents:
diff changeset
   122
  >> (fn (((x, pos), y), z) => (y, Args.src ((x, z), pos)));
69e8938c2409 Isar theory output.
wenzelm
parents:
diff changeset
   123
69e8938c2409 Isar theory output.
wenzelm
parents:
diff changeset
   124
fun antiq_args_aux keyword_lexicon (str, pos) =
69e8938c2409 Isar theory output.
wenzelm
parents:
diff changeset
   125
  Source.of_string str
69e8938c2409 Isar theory output.
wenzelm
parents:
diff changeset
   126
  |> Symbol.source false
69e8938c2409 Isar theory output.
wenzelm
parents:
diff changeset
   127
  |> T.source false (K (keyword_lexicon, Scan.empty_lexicon)) pos
69e8938c2409 Isar theory output.
wenzelm
parents:
diff changeset
   128
  |> T.source_proper
69e8938c2409 Isar theory output.
wenzelm
parents:
diff changeset
   129
  |> Source.source T.stopper (Scan.error (Scan.bulk (P.!!! antiq))) None
69e8938c2409 Isar theory output.
wenzelm
parents:
diff changeset
   130
  |> Source.exhaust;
69e8938c2409 Isar theory output.
wenzelm
parents:
diff changeset
   131
69e8938c2409 Isar theory output.
wenzelm
parents:
diff changeset
   132
in
69e8938c2409 Isar theory output.
wenzelm
parents:
diff changeset
   133
69e8938c2409 Isar theory output.
wenzelm
parents:
diff changeset
   134
fun antiq_args lex (s, pos) =
69e8938c2409 Isar theory output.
wenzelm
parents:
diff changeset
   135
  (case antiq_args_aux lex (s, pos) of [x] => x | _ => raise ERROR) handle ERROR =>
69e8938c2409 Isar theory output.
wenzelm
parents:
diff changeset
   136
    error ("Malformed antiquotation: " ^ quote ("@{" ^ s ^ "}") ^ Position.str_of pos);
69e8938c2409 Isar theory output.
wenzelm
parents:
diff changeset
   137
69e8938c2409 Isar theory output.
wenzelm
parents:
diff changeset
   138
end;
69e8938c2409 Isar theory output.
wenzelm
parents:
diff changeset
   139
69e8938c2409 Isar theory output.
wenzelm
parents:
diff changeset
   140
69e8938c2409 Isar theory output.
wenzelm
parents:
diff changeset
   141
(* eval_antiquote *)
69e8938c2409 Isar theory output.
wenzelm
parents:
diff changeset
   142
11714
bc0a84063a9c added global modes ref;
wenzelm
parents: 11524
diff changeset
   143
val modes = ref ([]: string list);
bc0a84063a9c added global modes ref;
wenzelm
parents: 11524
diff changeset
   144
9140
69e8938c2409 Isar theory output.
wenzelm
parents:
diff changeset
   145
fun eval_antiquote lex state (str, pos) =
69e8938c2409 Isar theory output.
wenzelm
parents:
diff changeset
   146
  let
69e8938c2409 Isar theory output.
wenzelm
parents:
diff changeset
   147
    fun expand (Antiquote.Text s) = s
69e8938c2409 Isar theory output.
wenzelm
parents:
diff changeset
   148
      | expand (Antiquote.Antiq x) =
69e8938c2409 Isar theory output.
wenzelm
parents:
diff changeset
   149
          let val (opts, src) = antiq_args lex x in
10739
ec19f5902ef5 antiq: preview errors;
wenzelm
parents: 10570
diff changeset
   150
            options opts (fn () => command src state) ();  (*preview errors!*)
11714
bc0a84063a9c added global modes ref;
wenzelm
parents: 11524
diff changeset
   151
            Library.setmp print_mode (! modes @ Latex.modes @ ! print_mode)
10570
fc7afc98a329 append print_modes;
wenzelm
parents: 10360
diff changeset
   152
              (options opts (fn () => command src state)) ()
10321
bbaad3045e37 let commands access Toplevel.state;
wenzelm
parents: 9863
diff changeset
   153
          end;
9140
69e8938c2409 Isar theory output.
wenzelm
parents:
diff changeset
   154
    val ants = Antiquote.antiquotes_of (str, pos);
69e8938c2409 Isar theory output.
wenzelm
parents:
diff changeset
   155
  in
69e8938c2409 Isar theory output.
wenzelm
parents:
diff changeset
   156
    if Toplevel.is_toplevel state andalso exists Antiquote.is_antiq ants then
69e8938c2409 Isar theory output.
wenzelm
parents:
diff changeset
   157
      error ("Cannot expand antiquotations at top-level" ^ Position.str_of pos)
69e8938c2409 Isar theory output.
wenzelm
parents:
diff changeset
   158
    else implode (map expand ants)
69e8938c2409 Isar theory output.
wenzelm
parents:
diff changeset
   159
  end;
69e8938c2409 Isar theory output.
wenzelm
parents:
diff changeset
   160
69e8938c2409 Isar theory output.
wenzelm
parents:
diff changeset
   161
69e8938c2409 Isar theory output.
wenzelm
parents:
diff changeset
   162
69e8938c2409 Isar theory output.
wenzelm
parents:
diff changeset
   163
(** present theory source **)
69e8938c2409 Isar theory output.
wenzelm
parents:
diff changeset
   164
69e8938c2409 Isar theory output.
wenzelm
parents:
diff changeset
   165
(* present_tokens *)
69e8938c2409 Isar theory output.
wenzelm
parents:
diff changeset
   166
69e8938c2409 Isar theory output.
wenzelm
parents:
diff changeset
   167
val interest_level = ref 0;
69e8938c2409 Isar theory output.
wenzelm
parents:
diff changeset
   168
11861
38d8075ebff6 maintain Latex.flag_markup;
wenzelm
parents: 11716
diff changeset
   169
fun present_tokens lex (flag, toks) state =
38d8075ebff6 maintain Latex.flag_markup;
wenzelm
parents: 11716
diff changeset
   170
  Buffer.add (case flag of None => "" | Some b => Latex.flag_markup b) o
38d8075ebff6 maintain Latex.flag_markup;
wenzelm
parents: 11716
diff changeset
   171
   (toks
38d8075ebff6 maintain Latex.flag_markup;
wenzelm
parents: 11716
diff changeset
   172
    |> mapfilter (fn (tk, i) => if i > ! interest_level then None else Some tk)
38d8075ebff6 maintain Latex.flag_markup;
wenzelm
parents: 11716
diff changeset
   173
    |> map (apsnd (eval_antiquote lex state))
38d8075ebff6 maintain Latex.flag_markup;
wenzelm
parents: 11716
diff changeset
   174
    |> Latex.output_tokens
38d8075ebff6 maintain Latex.flag_markup;
wenzelm
parents: 11716
diff changeset
   175
    |> Buffer.add);
9140
69e8938c2409 Isar theory output.
wenzelm
parents:
diff changeset
   176
69e8938c2409 Isar theory output.
wenzelm
parents:
diff changeset
   177
69e8938c2409 Isar theory output.
wenzelm
parents:
diff changeset
   178
(* parse_thy *)
69e8938c2409 Isar theory output.
wenzelm
parents:
diff changeset
   179
69e8938c2409 Isar theory output.
wenzelm
parents:
diff changeset
   180
datatype markup = Markup | MarkupEnv | Verbatim;
69e8938c2409 Isar theory output.
wenzelm
parents:
diff changeset
   181
69e8938c2409 Isar theory output.
wenzelm
parents:
diff changeset
   182
local
69e8938c2409 Isar theory output.
wenzelm
parents:
diff changeset
   183
69e8938c2409 Isar theory output.
wenzelm
parents:
diff changeset
   184
val opt_newline = Scan.option (Scan.one T.is_newline);
69e8938c2409 Isar theory output.
wenzelm
parents:
diff changeset
   185
69e8938c2409 Isar theory output.
wenzelm
parents:
diff changeset
   186
fun check_level i =
69e8938c2409 Isar theory output.
wenzelm
parents:
diff changeset
   187
  if i > 0 then Scan.succeed ()
69e8938c2409 Isar theory output.
wenzelm
parents:
diff changeset
   188
  else Scan.fail_with (K "Bad nesting of meta-comments");
69e8938c2409 Isar theory output.
wenzelm
parents:
diff changeset
   189
69e8938c2409 Isar theory output.
wenzelm
parents:
diff changeset
   190
val ignore =
13775
a918c547cd4d corrected swallowing of newlines after end-of-ignore: rollback
oheimb
parents: 13774
diff changeset
   191
  Scan.depend (fn i => opt_newline |-- P.position (Scan.one T.is_begin_ignore) >> pair (i + 1)) ||
a918c547cd4d corrected swallowing of newlines after end-of-ignore: rollback
oheimb
parents: 13774
diff changeset
   192
  Scan.depend (fn i => P.position (Scan.one T.is_end_ignore) --|
13774
77a1e723151d corrected swallowing of newlines after end-of-ignore (improved)
oheimb
parents: 13742
diff changeset
   193
    (opt_newline -- check_level i) >> pair (i - 1));
9140
69e8938c2409 Isar theory output.
wenzelm
parents:
diff changeset
   194
69e8938c2409 Isar theory output.
wenzelm
parents:
diff changeset
   195
val ignore_cmd = Scan.state -- ignore
11861
38d8075ebff6 maintain Latex.flag_markup;
wenzelm
parents: 11716
diff changeset
   196
  >> (fn (i, (x, pos)) => (false, (None, ((Latex.Basic x, ("", pos)), i))));
9140
69e8938c2409 Isar theory output.
wenzelm
parents:
diff changeset
   197
69e8938c2409 Isar theory output.
wenzelm
parents:
diff changeset
   198
69e8938c2409 Isar theory output.
wenzelm
parents:
diff changeset
   199
val is_improper = not o (T.is_proper orf T.is_begin_ignore orf T.is_end_ignore);
69e8938c2409 Isar theory output.
wenzelm
parents:
diff changeset
   200
val improper = Scan.any is_improper;
69e8938c2409 Isar theory output.
wenzelm
parents:
diff changeset
   201
69e8938c2409 Isar theory output.
wenzelm
parents:
diff changeset
   202
val improper_keep_indent = Scan.repeat
69e8938c2409 Isar theory output.
wenzelm
parents:
diff changeset
   203
  (Scan.unless (Scan.one T.is_indent -- Scan.one T.is_proper) (Scan.one is_improper));
69e8938c2409 Isar theory output.
wenzelm
parents:
diff changeset
   204
69e8938c2409 Isar theory output.
wenzelm
parents:
diff changeset
   205
val improper_end =
69e8938c2409 Isar theory output.
wenzelm
parents:
diff changeset
   206
  (improper -- P.semicolon) |-- improper_keep_indent ||
69e8938c2409 Isar theory output.
wenzelm
parents:
diff changeset
   207
  improper_keep_indent;
69e8938c2409 Isar theory output.
wenzelm
parents:
diff changeset
   208
69e8938c2409 Isar theory output.
wenzelm
parents:
diff changeset
   209
69e8938c2409 Isar theory output.
wenzelm
parents:
diff changeset
   210
val stopper =
11861
38d8075ebff6 maintain Latex.flag_markup;
wenzelm
parents: 11716
diff changeset
   211
  ((false, (None, ((Latex.Basic (#1 T.stopper), ("", Position.none)), 0))),
38d8075ebff6 maintain Latex.flag_markup;
wenzelm
parents: 11716
diff changeset
   212
    fn (_, (_, ((Latex.Basic x, _), _))) => (#2 T.stopper x) | _ => false);
9140
69e8938c2409 Isar theory output.
wenzelm
parents:
diff changeset
   213
69e8938c2409 Isar theory output.
wenzelm
parents:
diff changeset
   214
in
69e8938c2409 Isar theory output.
wenzelm
parents:
diff changeset
   215
69e8938c2409 Isar theory output.
wenzelm
parents:
diff changeset
   216
fun parse_thy markup lex trs src =
69e8938c2409 Isar theory output.
wenzelm
parents:
diff changeset
   217
  let
69e8938c2409 Isar theory output.
wenzelm
parents:
diff changeset
   218
    val text = P.position P.text;
9220
d0506ced27c8 added options "eta_contract", "long_names";
wenzelm
parents: 9213
diff changeset
   219
    val token = Scan.depend (fn i =>
9140
69e8938c2409 Isar theory output.
wenzelm
parents:
diff changeset
   220
     (improper |-- markup Markup -- P.!!!! (improper |-- text --| improper_end)
11861
38d8075ebff6 maintain Latex.flag_markup;
wenzelm
parents: 11716
diff changeset
   221
        >> (fn (x, y) => (true, (Some true, ((Latex.Markup (T.val_of x), y), i)))) ||
9140
69e8938c2409 Isar theory output.
wenzelm
parents:
diff changeset
   222
      improper |-- markup MarkupEnv -- P.!!!! (improper |-- text --| improper_end)
11861
38d8075ebff6 maintain Latex.flag_markup;
wenzelm
parents: 11716
diff changeset
   223
        >> (fn (x, y) => (true, (Some true, ((Latex.MarkupEnv (T.val_of x), y), i)))) ||
9140
69e8938c2409 Isar theory output.
wenzelm
parents:
diff changeset
   224
      (P.$$$ "--" |-- P.!!!! (improper |-- text))
11861
38d8075ebff6 maintain Latex.flag_markup;
wenzelm
parents: 11716
diff changeset
   225
        >> (fn y => (false, (None, ((Latex.Markup "cmt", y), i)))) ||
9140
69e8938c2409 Isar theory output.
wenzelm
parents:
diff changeset
   226
      (improper -- markup Verbatim) |-- P.!!!! (improper |-- text --| improper_end)
11861
38d8075ebff6 maintain Latex.flag_markup;
wenzelm
parents: 11716
diff changeset
   227
        >> (fn y => (true, (None, ((Latex.Verbatim, y), i)))) ||
9140
69e8938c2409 Isar theory output.
wenzelm
parents:
diff changeset
   228
      P.position (Scan.one T.not_eof)
11861
38d8075ebff6 maintain Latex.flag_markup;
wenzelm
parents: 11716
diff changeset
   229
        >> (fn (x, pos) => (T.is_kind T.Command x, (Some false, ((Latex.Basic x, ("", pos)), i)))))
9220
d0506ced27c8 added options "eta_contract", "long_names";
wenzelm
parents: 9213
diff changeset
   230
      >> pair i);
9140
69e8938c2409 Isar theory output.
wenzelm
parents:
diff changeset
   231
69e8938c2409 Isar theory output.
wenzelm
parents:
diff changeset
   232
    val body = Scan.any (not o fst andf not o #2 stopper);
11861
38d8075ebff6 maintain Latex.flag_markup;
wenzelm
parents: 11716
diff changeset
   233
    val section = body -- Scan.one fst -- body
38d8075ebff6 maintain Latex.flag_markup;
wenzelm
parents: 11716
diff changeset
   234
      >> (fn ((b1, c), b2) => (#1 (#2 c), map (snd o snd) (b1 @ (c :: b2))));
9140
69e8938c2409 Isar theory output.
wenzelm
parents:
diff changeset
   235
69e8938c2409 Isar theory output.
wenzelm
parents:
diff changeset
   236
    val cmds =
69e8938c2409 Isar theory output.
wenzelm
parents:
diff changeset
   237
      src
69e8938c2409 Isar theory output.
wenzelm
parents:
diff changeset
   238
      |> Source.filter (not o T.is_semicolon)
69e8938c2409 Isar theory output.
wenzelm
parents:
diff changeset
   239
      |> Source.source' 0 T.stopper (Scan.error (Scan.bulk (ignore_cmd || token))) None
69e8938c2409 Isar theory output.
wenzelm
parents:
diff changeset
   240
      |> Source.source stopper (Scan.error (Scan.bulk section)) None
69e8938c2409 Isar theory output.
wenzelm
parents:
diff changeset
   241
      |> Source.exhaust;
69e8938c2409 Isar theory output.
wenzelm
parents:
diff changeset
   242
  in
69e8938c2409 Isar theory output.
wenzelm
parents:
diff changeset
   243
    if length cmds = length trs then
69e8938c2409 Isar theory output.
wenzelm
parents:
diff changeset
   244
      (trs ~~ map (present_tokens lex) cmds, Buffer.empty)
11861
38d8075ebff6 maintain Latex.flag_markup;
wenzelm
parents: 11716
diff changeset
   245
    else error "Messed-up outer syntax for presentation"
9140
69e8938c2409 Isar theory output.
wenzelm
parents:
diff changeset
   246
  end;
69e8938c2409 Isar theory output.
wenzelm
parents:
diff changeset
   247
69e8938c2409 Isar theory output.
wenzelm
parents:
diff changeset
   248
end;
69e8938c2409 Isar theory output.
wenzelm
parents:
diff changeset
   249
69e8938c2409 Isar theory output.
wenzelm
parents:
diff changeset
   250
69e8938c2409 Isar theory output.
wenzelm
parents:
diff changeset
   251
69e8938c2409 Isar theory output.
wenzelm
parents:
diff changeset
   252
(** setup default output **)
69e8938c2409 Isar theory output.
wenzelm
parents:
diff changeset
   253
69e8938c2409 Isar theory output.
wenzelm
parents:
diff changeset
   254
(* options *)
69e8938c2409 Isar theory output.
wenzelm
parents:
diff changeset
   255
69e8938c2409 Isar theory output.
wenzelm
parents:
diff changeset
   256
val display = ref false;
69e8938c2409 Isar theory output.
wenzelm
parents:
diff changeset
   257
val quotes = ref false;
9732
c32c7ef228c6 added "name" antiq and "indent" option;
wenzelm
parents: 9504
diff changeset
   258
val indent = ref 0;
9750
270cd9831e7b added "source" option;
wenzelm
parents: 9732
diff changeset
   259
val source = ref false;
13929
21615e44ba88 Added "break" flag to allow line breaks within \isa{...}
berghofe
parents: 13775
diff changeset
   260
val break = ref false;
9140
69e8938c2409 Isar theory output.
wenzelm
parents:
diff changeset
   261
69e8938c2409 Isar theory output.
wenzelm
parents:
diff changeset
   262
val _ = add_options
9220
d0506ced27c8 added options "eta_contract", "long_names";
wenzelm
parents: 9213
diff changeset
   263
 [("show_types", Library.setmp Syntax.show_types o boolean),
d0506ced27c8 added options "eta_contract", "long_names";
wenzelm
parents: 9213
diff changeset
   264
  ("show_sorts", Library.setmp Syntax.show_sorts o boolean),
14707
2d6350d7b9b7 show_structs option;
wenzelm
parents: 14696
diff changeset
   265
  ("show_structs", Library.setmp show_structs o boolean),
14696
wenzelm
parents: 14345
diff changeset
   266
  ("long_names", Library.setmp NameSpace.long_names o boolean),
9220
d0506ced27c8 added options "eta_contract", "long_names";
wenzelm
parents: 9213
diff changeset
   267
  ("eta_contract", Library.setmp Syntax.eta_contract o boolean),
9140
69e8938c2409 Isar theory output.
wenzelm
parents:
diff changeset
   268
  ("display", Library.setmp display o boolean),
13929
21615e44ba88 Added "break" flag to allow line breaks within \isa{...}
berghofe
parents: 13775
diff changeset
   269
  ("break", Library.setmp break o boolean),
9140
69e8938c2409 Isar theory output.
wenzelm
parents:
diff changeset
   270
  ("quotes", Library.setmp quotes o boolean),
69e8938c2409 Isar theory output.
wenzelm
parents:
diff changeset
   271
  ("mode", fn s => fn f => fn () => Library.setmp print_mode (s :: ! print_mode) f ()),
9732
c32c7ef228c6 added "name" antiq and "indent" option;
wenzelm
parents: 9504
diff changeset
   272
  ("margin", Pretty.setmp_margin o integer),
9750
270cd9831e7b added "source" option;
wenzelm
parents: 9732
diff changeset
   273
  ("indent", Library.setmp indent o integer),
10321
bbaad3045e37 let commands access Toplevel.state;
wenzelm
parents: 9863
diff changeset
   274
  ("source", Library.setmp source o boolean),
bbaad3045e37 let commands access Toplevel.state;
wenzelm
parents: 9863
diff changeset
   275
  ("goals_limit", Library.setmp goals_limit o integer)];
9140
69e8938c2409 Isar theory output.
wenzelm
parents:
diff changeset
   276
69e8938c2409 Isar theory output.
wenzelm
parents:
diff changeset
   277
69e8938c2409 Isar theory output.
wenzelm
parents:
diff changeset
   278
(* commands *)
69e8938c2409 Isar theory output.
wenzelm
parents:
diff changeset
   279
69e8938c2409 Isar theory output.
wenzelm
parents:
diff changeset
   280
fun cond_quote prt =
69e8938c2409 Isar theory output.
wenzelm
parents:
diff changeset
   281
  if ! quotes then Pretty.quote prt else prt;
69e8938c2409 Isar theory output.
wenzelm
parents:
diff changeset
   282
69e8938c2409 Isar theory output.
wenzelm
parents:
diff changeset
   283
fun cond_display prt =
69e8938c2409 Isar theory output.
wenzelm
parents:
diff changeset
   284
  if ! display then
9732
c32c7ef228c6 added "name" antiq and "indent" option;
wenzelm
parents: 9504
diff changeset
   285
    Pretty.string_of (Pretty.indent (! indent) prt)
9863
67cdb658e422 tuned output of isabelle env;
wenzelm
parents: 9828
diff changeset
   286
    |> enclose "\\begin{isabelle}%\n" "%\n\\end{isabelle}"
9140
69e8938c2409 Isar theory output.
wenzelm
parents:
diff changeset
   287
  else
13929
21615e44ba88 Added "break" flag to allow line breaks within \isa{...}
berghofe
parents: 13775
diff changeset
   288
    (if ! break then Pretty.string_of else Pretty.str_of) prt
9140
69e8938c2409 Isar theory output.
wenzelm
parents:
diff changeset
   289
    |> enclose "\\isa{" "}";
69e8938c2409 Isar theory output.
wenzelm
parents:
diff changeset
   290
14345
3023d90dc59e separate thm lists in latex output by \isasep
kleing
parents: 13929
diff changeset
   291
fun cond_seq_display prts =
3023d90dc59e separate thm lists in latex output by \isasep
kleing
parents: 13929
diff changeset
   292
  if ! display then
3023d90dc59e separate thm lists in latex output by \isasep
kleing
parents: 13929
diff changeset
   293
    map (Pretty.string_of o Pretty.indent (! indent)) prts
3023d90dc59e separate thm lists in latex output by \isasep
kleing
parents: 13929
diff changeset
   294
    |> separate "\\isasep\\isanewline%\n"
3023d90dc59e separate thm lists in latex output by \isasep
kleing
parents: 13929
diff changeset
   295
    |> implode
3023d90dc59e separate thm lists in latex output by \isasep
kleing
parents: 13929
diff changeset
   296
    |> enclose "\\begin{isabelle}%\n" "%\n\\end{isabelle}"
3023d90dc59e separate thm lists in latex output by \isasep
kleing
parents: 13929
diff changeset
   297
  else
3023d90dc59e separate thm lists in latex output by \isasep
kleing
parents: 13929
diff changeset
   298
    map (if ! break then Pretty.string_of else Pretty.str_of) prts
3023d90dc59e separate thm lists in latex output by \isasep
kleing
parents: 13929
diff changeset
   299
    |> separate "\\isasep\\isanewline%\n"
3023d90dc59e separate thm lists in latex output by \isasep
kleing
parents: 13929
diff changeset
   300
    |> implode
3023d90dc59e separate thm lists in latex output by \isasep
kleing
parents: 13929
diff changeset
   301
    |> enclose "\\isa{" "}";
3023d90dc59e separate thm lists in latex output by \isasep
kleing
parents: 13929
diff changeset
   302
11011
14b78c0c9f05 pretty_text: tweak_lines handles linebreaks gracefully;
wenzelm
parents: 10739
diff changeset
   303
fun tweak_line s =
14b78c0c9f05 pretty_text: tweak_lines handles linebreaks gracefully;
wenzelm
parents: 10739
diff changeset
   304
  if ! display then s else Symbol.strip_blanks s;
9750
270cd9831e7b added "source" option;
wenzelm
parents: 9732
diff changeset
   305
11011
14b78c0c9f05 pretty_text: tweak_lines handles linebreaks gracefully;
wenzelm
parents: 10739
diff changeset
   306
val pretty_text = Pretty.chunks o map Pretty.str o map tweak_line o Library.split_lines;
9140
69e8938c2409 Isar theory output.
wenzelm
parents:
diff changeset
   307
9750
270cd9831e7b added "source" option;
wenzelm
parents: 9732
diff changeset
   308
val pretty_source =
270cd9831e7b added "source" option;
wenzelm
parents: 9732
diff changeset
   309
  pretty_text o space_implode " " o map Args.string_of o #2 o #1 o Args.dest_src;
9140
69e8938c2409 Isar theory output.
wenzelm
parents:
diff changeset
   310
12055
a9c44895cc8c pretty/print functions with context;
wenzelm
parents: 11861
diff changeset
   311
fun pretty_term ctxt = ProofContext.pretty_term ctxt o ProofContext.extern_skolem ctxt;
9140
69e8938c2409 Isar theory output.
wenzelm
parents:
diff changeset
   312
14345
3023d90dc59e separate thm lists in latex output by \isasep
kleing
parents: 13929
diff changeset
   313
fun pretty_thm ctxt = pretty_term ctxt o Thm.prop_of;
9140
69e8938c2409 Isar theory output.
wenzelm
parents:
diff changeset
   314
12055
a9c44895cc8c pretty/print functions with context;
wenzelm
parents: 11861
diff changeset
   315
fun pretty_prf full ctxt thms =    (* FIXME context syntax!? *)
11524
197f2e14a714 Added functions for printing primitive proof terms.
berghofe
parents: 11240
diff changeset
   316
  Pretty.chunks (map (ProofSyntax.pretty_proof_of full) thms);
197f2e14a714 Added functions for printing primitive proof terms.
berghofe
parents: 11240
diff changeset
   317
9750
270cd9831e7b added "source" option;
wenzelm
parents: 9732
diff changeset
   318
fun output_with pretty src ctxt x =
270cd9831e7b added "source" option;
wenzelm
parents: 9732
diff changeset
   319
  let
12055
a9c44895cc8c pretty/print functions with context;
wenzelm
parents: 11861
diff changeset
   320
    val prt = pretty ctxt x;      (*always pretty in order to catch errors!*)
9750
270cd9831e7b added "source" option;
wenzelm
parents: 9732
diff changeset
   321
    val prt' = if ! source then pretty_source src else prt;
270cd9831e7b added "source" option;
wenzelm
parents: 9732
diff changeset
   322
  in cond_display (cond_quote prt') end;
9732
c32c7ef228c6 added "name" antiq and "indent" option;
wenzelm
parents: 9504
diff changeset
   323
14345
3023d90dc59e separate thm lists in latex output by \isasep
kleing
parents: 13929
diff changeset
   324
fun output_seq_with pretty src ctxt xs =
3023d90dc59e separate thm lists in latex output by \isasep
kleing
parents: 13929
diff changeset
   325
  let
3023d90dc59e separate thm lists in latex output by \isasep
kleing
parents: 13929
diff changeset
   326
    val prts = map (pretty ctxt) xs;   (*always pretty in order to catch errors!*)
3023d90dc59e separate thm lists in latex output by \isasep
kleing
parents: 13929
diff changeset
   327
    val prts' = if ! source then [pretty_source src] else prts;
3023d90dc59e separate thm lists in latex output by \isasep
kleing
parents: 13929
diff changeset
   328
  in cond_seq_display (map cond_quote prts') end;
3023d90dc59e separate thm lists in latex output by \isasep
kleing
parents: 13929
diff changeset
   329
10360
807992b67edd tuned goals output;
wenzelm
parents: 10350
diff changeset
   330
fun output_goals main_goal src state = args (Scan.succeed ()) (output_with (fn _ => fn _ =>
807992b67edd tuned goals output;
wenzelm
parents: 10350
diff changeset
   331
  Pretty.chunks (Proof.pretty_goals main_goal (Toplevel.proof_of state
807992b67edd tuned goals output;
wenzelm
parents: 10350
diff changeset
   332
      handle Toplevel.UNDEF => error "No proof state")))) src state;
807992b67edd tuned goals output;
wenzelm
parents: 10350
diff changeset
   333
9140
69e8938c2409 Isar theory output.
wenzelm
parents:
diff changeset
   334
val _ = add_commands
14696
wenzelm
parents: 14345
diff changeset
   335
 [("thm", args Attrib.local_thmss (output_seq_with pretty_thm)),
9750
270cd9831e7b added "source" option;
wenzelm
parents: 9732
diff changeset
   336
  ("prop", args Args.local_prop (output_with pretty_term)),
270cd9831e7b added "source" option;
wenzelm
parents: 9732
diff changeset
   337
  ("term", args Args.local_term (output_with pretty_term)),
14776
4f3b383a46ae Args.local_typ_raw;
wenzelm
parents: 14707
diff changeset
   338
  ("typ", args Args.local_typ_raw (output_with ProofContext.pretty_typ)),
14696
wenzelm
parents: 14345
diff changeset
   339
  ("text", args (Scan.lift Args.name) (output_with (K pretty_text))),
10360
807992b67edd tuned goals output;
wenzelm
parents: 10350
diff changeset
   340
  ("goals", output_goals true),
14696
wenzelm
parents: 14345
diff changeset
   341
  ("subgoals", output_goals false),
wenzelm
parents: 14345
diff changeset
   342
  ("prf", args Attrib.local_thmss (output_with (pretty_prf false))),
wenzelm
parents: 14345
diff changeset
   343
  ("full_prf", args Attrib.local_thmss (output_with (pretty_prf true)))];
9140
69e8938c2409 Isar theory output.
wenzelm
parents:
diff changeset
   344
69e8938c2409 Isar theory output.
wenzelm
parents:
diff changeset
   345
end;