# HG changeset patch
# User wenzelm
# Date 961970249 -7200
# Node ID 69e8938c24090675d6756a0bdeaf6a423c7e7b1d
# Parent  bf272b4985ec031b33efb4f679084812fa867c46
Isar theory output.

diff -r bf272b4985ec -r 69e8938c2409 src/Pure/Isar/isar_output.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/Isar/isar_output.ML	Sun Jun 25 23:57:29 2000 +0200
@@ -0,0 +1,286 @@
+(*  Title:      Pure/Isar/isar_output.ML
+    ID:         $Id$
+    Author:     Markus Wenzel, TU Muenchen
+    License:    GPL (GNU GENERAL PUBLIC LICENSE)
+
+Isar theory output.
+*)
+
+signature ISAR_OUTPUT =
+sig
+  val add_commands: (string * (Args.src -> Proof.context -> string)) list -> unit
+  val add_options: (string * (string -> (unit -> string) -> unit -> string)) list -> unit
+  val boolean: string -> bool
+  val integer: string -> int
+  val args: (Proof.context * Args.T list -> 'a * (Proof.context * Args.T list)) ->
+    (Proof.context -> 'a -> string) -> Args.src -> Proof.context -> string
+  datatype markup = Markup | MarkupEnv | Verbatim
+  val interest_level: int ref
+  val parse_thy: (markup -> OuterLex.token list -> OuterLex.token * OuterLex.token list) ->
+    Scan.lexicon -> Toplevel.transition list -> (OuterLex.token, 'a) Source.source ->
+      (Toplevel.transition * (Toplevel.state -> Buffer.T -> Buffer.T)) list * Buffer.T
+  val display: bool ref
+  val quotes: bool ref
+end;
+
+structure IsarOutput: ISAR_OUTPUT =
+struct
+
+structure T = OuterLex;
+structure P = OuterParse;
+
+
+(** maintain global commands **)
+
+local
+
+val global_commands =
+  ref (Symtab.empty: (Args.src -> Proof.context -> string) Symtab.table);
+
+val global_options =
+  ref (Symtab.empty: (string -> (unit -> string) -> unit -> string) Symtab.table);
+
+
+fun add_item kind (tab, (name, x)) =
+ (if is_none (Symtab.lookup (tab, name)) then ()
+  else warning ("Redefined antiquotation output " ^ kind ^ ": " ^ quote name);
+  Symtab.update ((name, x), tab));
+
+fun add_items kind xs tab = foldl (add_item kind) (tab, xs);
+
+in
+
+val add_commands = Library.change global_commands o (add_items "command");
+val add_options = Library.change global_options o (add_items "option");
+
+fun command src =
+  let val ((name, _), pos) = Args.dest_src src in
+    (case Symtab.lookup (! global_commands, name) of
+      None => error ("Unknown antiquotation command: " ^ quote name ^ Position.str_of pos)
+    | Some f => transform_failure (curry Comment.OUTPUT_FAIL (name, pos)) (f src))
+  end;
+
+fun option (name, s) f () =
+  (case Symtab.lookup (! global_options, name) of
+    None => error ("Unknown antiquotation option: " ^ quote name)
+  | Some opt => opt s f ());
+
+fun options [] f = f
+  | options (opt :: opts) f = option opt (options opts f);
+
+end;
+
+
+
+(** syntax of antiquotations **)
+
+(* option values *)
+
+fun boolean "" = true
+  | boolean "true" = true
+  | boolean "false" = false
+  | boolean s = error ("Bad boolean value: " ^ quote s);
+
+fun integer s =
+  let
+    fun int ss =
+      (case Term.read_int ss of (i, []) => i | _ => error ("Bad integer value: " ^ quote s));
+  in (case Symbol.explode s of "-" :: ss => ~ (int ss) | ss => int ss) end;
+
+
+(* args syntax *)
+
+fun syntax (scan: (Proof.context * Args.T list -> 'a * (Proof.context * Args.T list))) =
+  Args.syntax "antiquotation" scan;
+
+fun args scan f src ctxt : string =
+  let val (ctxt', x) = syntax scan src ctxt
+  in f ctxt' x end;
+
+
+(* outer syntax *)
+
+local
+
+val property = P.xname -- Scan.optional (P.$$$ "=" |-- P.!!! P.xname) "";
+val properties = Scan.optional (P.$$$ "[" |-- P.!!! (P.enum "," property --| P.$$$ "]")) [];
+
+val antiq = P.position P.xname -- properties -- P.arguments --| Scan.ahead P.eof
+  >> (fn (((x, pos), y), z) => (y, Args.src ((x, z), pos)));
+
+fun antiq_args_aux keyword_lexicon (str, pos) =
+  Source.of_string str
+  |> Symbol.source false
+  |> T.source false (K (keyword_lexicon, Scan.empty_lexicon)) pos
+  |> T.source_proper
+  |> Source.source T.stopper (Scan.error (Scan.bulk (P.!!! antiq))) None
+  |> Source.exhaust;
+
+in
+
+fun antiq_args lex (s, pos) =
+  (case antiq_args_aux lex (s, pos) of [x] => x | _ => raise ERROR) handle ERROR =>
+    error ("Malformed antiquotation: " ^ quote ("@{" ^ s ^ "}") ^ Position.str_of pos);
+
+end;
+
+
+(* eval_antiquote *)
+
+fun eval_antiquote lex state (str, pos) =
+  let
+    fun expand (Antiquote.Text s) = s
+      | expand (Antiquote.Antiq x) =
+          let val (opts, src) = antiq_args lex x in
+            Library.setmp print_mode Latex.modes   (*note: lazy lookup of context below!*)
+              (options opts (fn () => command src (Toplevel.context_of state))) () end;
+    val ants = Antiquote.antiquotes_of (str, pos);
+  in
+    if Toplevel.is_toplevel state andalso exists Antiquote.is_antiq ants then
+      error ("Cannot expand antiquotations at top-level" ^ Position.str_of pos)
+    else implode (map expand ants)
+  end;
+
+
+
+(** present theory source **)
+
+(* present_tokens *)
+
+val interest_level = ref 0;
+
+fun present_tokens lex toks state =
+  toks
+  |> mapfilter (fn (tk, i) => if i > ! interest_level then None else Some tk)
+  |> map (apsnd (eval_antiquote lex state))
+  |> Latex.output_tokens
+  |> Buffer.add;
+
+
+(* parse_thy *)
+
+datatype markup = Markup | MarkupEnv | Verbatim;
+
+local
+
+val opt_newline = Scan.option (Scan.one T.is_newline);
+
+fun check_level i =
+  if i > 0 then Scan.succeed ()
+  else Scan.fail_with (K "Bad nesting of meta-comments");
+
+val ignore =
+  Scan.depend (fn i => opt_newline |-- P.position (Scan.one T.is_begin_ignore) >> pair (i + 1)) ||
+  Scan.depend (fn i => P.position (Scan.one T.is_end_ignore) --|
+    (opt_newline -- check_level i) >> pair (i - 1));
+
+val ignore_cmd = Scan.state -- ignore
+  >> (fn (i, (x, pos)) => (false, ((Latex.Basic x, ("", pos)), i)));
+
+
+val is_improper = not o (T.is_proper orf T.is_begin_ignore orf T.is_end_ignore);
+val improper = Scan.any is_improper;
+
+val improper_keep_indent = Scan.repeat
+  (Scan.unless (Scan.one T.is_indent -- Scan.one T.is_proper) (Scan.one is_improper));
+
+val improper_end =
+  (improper -- P.semicolon) |-- improper_keep_indent ||
+  improper_keep_indent;
+
+
+val stopper =
+  ((false, ((Latex.Basic (#1 T.stopper), ("", Position.none)), 0)),
+    fn (_, ((Latex.Basic x, _), _)) => (#2 T.stopper x) | _ => false);
+
+in
+
+fun parse_thy markup lex trs src =
+  let
+    val text = P.position P.text;
+    val token = Scan.state :-- (fn i => Scan.lift
+     (improper |-- markup Markup -- P.!!!! (improper |-- text --| improper_end)
+        >> (fn (x, y) => (true, ((Latex.Markup (T.val_of x), y), i))) ||
+      improper |-- markup MarkupEnv -- P.!!!! (improper |-- text --| improper_end)
+        >> (fn (x, y) => (true, ((Latex.MarkupEnv (T.val_of x), y), i))) ||
+      (P.$$$ "--" |-- P.!!!! (improper |-- text))
+        >> (fn y => (false, ((Latex.Markup "cmt", y), i))) ||
+      (improper -- markup Verbatim) |-- P.!!!! (improper |-- text --| improper_end)
+        >> (fn y => (true, ((Latex.Verbatim, y), i))) ||
+      P.position (Scan.one T.not_eof)
+        >> (fn (x, pos) => (T.is_kind T.Command x, ((Latex.Basic x, ("", pos)), i)))))
+      >> #2;
+
+    val body = Scan.any (not o fst andf not o #2 stopper);
+    val section = body -- Scan.one fst -- body >> (fn ((x, y), z) => map snd (x @ (y :: z)));
+
+    val cmds =
+      src
+      |> Source.filter (not o T.is_semicolon)
+      |> Source.source' 0 T.stopper (Scan.error (Scan.bulk (ignore_cmd || token))) None
+      |> Source.source stopper (Scan.error (Scan.bulk section)) None
+      |> Source.exhaust;
+  in
+    if length cmds = length trs then
+      (trs ~~ map (present_tokens lex) cmds, Buffer.empty)
+    else error "Messed up outer syntax for presentation"
+  end;
+
+end;
+
+
+
+(** setup default output **)
+
+(* options *)
+
+val display = ref false;
+val quotes = ref false;
+
+val _ = add_options
+ [("show_types", Library.setmp show_types o boolean),
+  ("show_sorts", Library.setmp show_sorts o boolean),
+  ("display", Library.setmp display o boolean),
+  ("quotes", Library.setmp quotes o boolean),
+  ("mode", fn s => fn f => fn () => Library.setmp print_mode (s :: ! print_mode) f ()),
+  ("margin", Pretty.setmp_margin o integer)];
+
+
+(* commands *)
+
+local
+
+fun cond_quote prt =
+  if ! quotes then Pretty.quote prt else prt;
+
+fun cond_display prt =
+  if ! display then
+    Pretty.string_of prt
+    |> enclose "\n\\begin{isabelle}%\n" "\n\\end{isabelle}%\n"
+  else
+    Pretty.str_of prt
+    |> enclose "\\isa{" "}";
+
+val string_of = cond_display o cond_quote;
+
+
+fun pretty_typ ctxt T =
+  Sign.pretty_typ (ProofContext.sign_of ctxt) T;
+
+fun pretty_term ctxt t =
+  Sign.pretty_term (ProofContext.sign_of ctxt) (ProofContext.extern_skolem ctxt t);
+
+fun pretty_thm ctxt thms =
+  Pretty.chunks (map (pretty_term ctxt o #prop o Thm.rep_thm) thms);
+
+in
+
+val _ = add_commands
+ [("thm", args Attrib.local_thms (string_of oo pretty_thm)),
+  ("prop", args Args.local_prop (string_of oo pretty_term)),
+  ("term", args Args.local_term (string_of oo pretty_term)),
+  ("typ", args Args.local_typ (string_of oo pretty_typ))];
+
+end;
+
+end;