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