src/Pure/Thy/thy_output.ML
changeset 30390 ad591ee76c78
parent 30381 a59d792d0ccf
child 30394 c11a1e65a2ed
     1.1 --- a/src/Pure/Thy/thy_output.ML	Mon Mar 09 15:49:55 2009 +0100
     1.2 +++ b/src/Pure/Thy/thy_output.ML	Mon Mar 09 17:53:53 2009 +0100
     1.3 @@ -1,7 +1,7 @@
     1.4  (*  Title:      Pure/Thy/thy_output.ML
     1.5      Author:     Markus Wenzel, TU Muenchen
     1.6  
     1.7 -Theory document output.
     1.8 +Theory document output with antiquotations.
     1.9  *)
    1.10  
    1.11  signature THY_OUTPUT =
    1.12 @@ -21,20 +21,17 @@
    1.13    val antiquotation: string ->
    1.14      (Context.generic * Args.T list -> 'a * (Context.generic * Args.T list)) ->
    1.15      ({state: Toplevel.state, source: Args.src, context: Proof.context} -> 'a -> string) -> unit
    1.16 -  val args: (Context.generic * Args.T list -> 'a * (Context.generic * Args.T list)) ->
    1.17 -    (Args.src -> Proof.context -> 'a -> string) -> Args.src -> Toplevel.state -> string
    1.18    datatype markup = Markup | MarkupEnv | Verbatim
    1.19    val modes: string list ref
    1.20    val eval_antiquote: Scan.lexicon -> Toplevel.state -> SymbolPos.text * Position.T -> string
    1.21    val present_thy: Scan.lexicon -> (string -> string list) -> (markup -> string -> bool) ->
    1.22      (Toplevel.transition * Toplevel.state) list -> (OuterLex.token, 'a) Source.source -> Buffer.T
    1.23 -  val str_of_source: Args.src -> string
    1.24    val pretty_text: string -> Pretty.T
    1.25    val pretty_term: Proof.context -> term -> Pretty.T
    1.26    val pretty_thm: Proof.context -> thm -> Pretty.T
    1.27 -  val output_list: (Proof.context -> 'a -> Pretty.T) -> Args.src ->
    1.28 -    Proof.context -> 'a list -> string
    1.29 -  val output: (Proof.context -> 'a -> Pretty.T) -> Args.src -> Proof.context -> 'a -> string
    1.30 +  val str_of_source: Args.src -> string
    1.31 +  val maybe_pretty_source: ('a -> Pretty.T) -> Args.src -> 'a list -> Pretty.T list
    1.32 +  val output: Pretty.T list -> string
    1.33  end;
    1.34  
    1.35  structure ThyOutput: THY_OUTPUT =
    1.36 @@ -46,7 +43,6 @@
    1.37  
    1.38  (** global options **)
    1.39  
    1.40 -val locale = ref "";
    1.41  val display = ref false;
    1.42  val quotes = ref false;
    1.43  val indent = ref 0;
    1.44 @@ -55,7 +51,7 @@
    1.45  
    1.46  
    1.47  
    1.48 -(** maintain global commands **)
    1.49 +(** maintain global antiquotations **)
    1.50  
    1.51  local
    1.52  
    1.53 @@ -107,6 +103,11 @@
    1.54  
    1.55  end;
    1.56  
    1.57 +fun antiquotation name scan out = add_commands [(name, fn src => fn state =>
    1.58 +  let val (x, ctxt) = Args.context_syntax "document antiquotation"
    1.59 +    scan src (Toplevel.presentation_context_of state NONE)
    1.60 +  in out {source = src, state = state, context = ctxt} x end)];
    1.61 +
    1.62  
    1.63  
    1.64  (** syntax of antiquotations **)
    1.65 @@ -126,22 +127,6 @@
    1.66    in (case Symbol.explode s of "-" :: ss => ~ (int ss) | ss => int ss) end;
    1.67  
    1.68  
    1.69 -(* args syntax *)
    1.70 -
    1.71 -fun syntax scan = Args.context_syntax "document antiquotation" scan;
    1.72 -
    1.73 -fun antiquotation name scan output =
    1.74 -  add_commands [(name, fn src => fn state =>
    1.75 -    let val (x, ctxt) = syntax scan src (Toplevel.presentation_context_of state NONE);
    1.76 -    in output {source = src, state = state, context = ctxt} x end)];
    1.77 -
    1.78 -fun args scan f src state : string =
    1.79 -  let
    1.80 -    val loc = if ! locale = "" then NONE else SOME (! locale);
    1.81 -    val (x, ctxt) = syntax scan src (Toplevel.presentation_context_of state loc);
    1.82 -  in f src ctxt x end;
    1.83 -
    1.84 -
    1.85  (* outer syntax *)
    1.86  
    1.87  local
    1.88 @@ -438,7 +423,6 @@
    1.89    ("short_names", Library.setmp NameSpace.short_names o boolean),
    1.90    ("unique_names", Library.setmp NameSpace.unique_names o boolean),
    1.91    ("eta_contract", Library.setmp Syntax.eta_contract o boolean),
    1.92 -  ("locale", Library.setmp locale),
    1.93    ("display", Library.setmp display o boolean),
    1.94    ("break", Library.setmp break o boolean),
    1.95    ("quotes", Library.setmp quotes o boolean),
    1.96 @@ -451,8 +435,6 @@
    1.97  
    1.98  (* basic pretty printing *)
    1.99  
   1.100 -val str_of_source = space_implode " " o map T.unparse o #2 o #1 o Args.dest_src;
   1.101 -
   1.102  fun tweak_line s =
   1.103    if ! display then s else Symbol.strip_blanks s;
   1.104  
   1.105 @@ -493,18 +475,22 @@
   1.106  fun pretty_thm_style ctxt (name, th) =
   1.107    pretty_term_style ctxt (name, Thm.full_prop_of th);
   1.108  
   1.109 -fun pretty_prf full ctxt thms =
   1.110 -  Pretty.chunks (map (ProofSyntax.pretty_proof_of ctxt full) thms);
   1.111 +fun pretty_prf full ctxt = ProofSyntax.pretty_proof_of ctxt full;
   1.112  
   1.113  fun pretty_theory ctxt name =
   1.114    (Theory.requires (ProofContext.theory_of ctxt) name "presentation"; Pretty.str name);
   1.115  
   1.116  
   1.117 -(* Isar output *)
   1.118 +(* default output *)
   1.119 +
   1.120 +val str_of_source = space_implode " " o map T.unparse o #2 o #1 o Args.dest_src;
   1.121  
   1.122 -fun output_list pretty src ctxt xs =
   1.123 -  map (pretty ctxt) xs        (*always pretty in order to exhibit errors!*)
   1.124 -  |> (if ! source then K [pretty_text (str_of_source src)] else I)
   1.125 +fun maybe_pretty_source pretty src xs =
   1.126 +  map pretty xs  (*always pretty in order to exhibit errors!*)
   1.127 +  |> (if ! source then K [pretty_text (str_of_source src)] else I);
   1.128 +
   1.129 +fun output prts =
   1.130 +  prts
   1.131    |> (if ! quotes then map Pretty.quote else I)
   1.132    |> (if ! display then
   1.133      map (Output.output o Pretty.string_of o Pretty.indent (! indent))
   1.134 @@ -515,69 +501,98 @@
   1.135      #> space_implode "\\isasep\\isanewline%\n"
   1.136      #> enclose "\\isa{" "}");
   1.137  
   1.138 -fun output pretty src ctxt = output_list pretty src ctxt o single;
   1.139 +
   1.140 +
   1.141 +(** concrete antiquotations **)
   1.142 +
   1.143 +(* basic entities *)
   1.144 +
   1.145 +local
   1.146 +
   1.147 +fun basic_entities name scan pretty = antiquotation name scan
   1.148 +  (fn {source, context, ...} => output o maybe_pretty_source (pretty context) source);
   1.149 +
   1.150 +fun basic_entity name scan = basic_entities name (scan >> single);
   1.151 +
   1.152 +in
   1.153 +
   1.154 +val _ = basic_entities "thm" Attrib.thms pretty_thm;
   1.155 +val _ = basic_entity "thm_style" (Scan.lift Args.liberal_name -- Attrib.thm) pretty_thm_style;
   1.156 +val _ = basic_entity "prop" Args.prop pretty_term;
   1.157 +val _ = basic_entity "term" Args.term pretty_term;
   1.158 +val _ = basic_entity "term_style" (Scan.lift Args.liberal_name -- Args.term) pretty_term_style;
   1.159 +val _ = basic_entity "term_type" Args.term pretty_term_typ;
   1.160 +val _ = basic_entity "typeof" Args.term pretty_term_typeof;
   1.161 +val _ = basic_entity "const" Args.const_proper pretty_const;
   1.162 +val _ = basic_entity "abbrev" (Scan.lift Args.name_source) pretty_abbrev;
   1.163 +val _ = basic_entity "typ" Args.typ_abbrev Syntax.pretty_typ;
   1.164 +val _ = basic_entity "text" (Scan.lift Args.name) (K pretty_text);
   1.165 +val _ = basic_entities "prf" Attrib.thms (pretty_prf false);
   1.166 +val _ = basic_entities "full_prf" Attrib.thms (pretty_prf true);
   1.167 +val _ = basic_entity "theory" (Scan.lift Args.name) pretty_theory;
   1.168 +
   1.169 +end;
   1.170 +
   1.171 +
   1.172 +(* goal state *)
   1.173 +
   1.174 +local
   1.175  
   1.176  fun proof_state state =
   1.177    (case try Toplevel.proof_of state of
   1.178      SOME prf => prf
   1.179    | _ => error "No proof state");
   1.180  
   1.181 -fun output_goals main_goal src state = args (Scan.succeed ()) (output (fn _ => fn _ =>
   1.182 -  Pretty.chunks (Proof.pretty_goals main_goal (proof_state state)))) src state;
   1.183 -
   1.184 -fun ml_val txt = "fn _ => (" ^ txt ^ ");";
   1.185 -fun ml_type txt = "val _ = NONE : (" ^ txt ^ ") option;";
   1.186 -fun ml_struct txt = "functor DUMMY_FUNCTOR() = struct structure DUMMY = " ^ txt ^ " end;"
   1.187 +fun goal_state name main_goal = antiquotation name (Scan.succeed ())
   1.188 +  (fn {state, ...} => fn () => output
   1.189 +    [Pretty.chunks (Proof.pretty_goals main_goal (proof_state state))]);
   1.190  
   1.191 -fun output_ml ml _ ctxt (txt, pos) =
   1.192 - (ML_Context.eval_in (SOME ctxt) false pos (ml txt);
   1.193 -  SymbolPos.content (SymbolPos.explode (txt, pos))
   1.194 -  |> (if ! quotes then quote else I)
   1.195 -  |> (if ! display then enclose "\\begin{verbatim}\n" "\n\\end{verbatim}"
   1.196 -  else
   1.197 -    split_lines
   1.198 -    #> map (space_implode "\\verb,|," o map (enclose "\\verb|" "|") o space_explode "|")
   1.199 -    #> space_implode "\\isasep\\isanewline%\n"));
   1.200 +in
   1.201 +
   1.202 +val _ = goal_state "goals" true;
   1.203 +val _ = goal_state "subgoals" false;
   1.204 +
   1.205 +end;
   1.206  
   1.207  
   1.208 -(* embedded lemmas *)
   1.209 -
   1.210 -fun pretty_lemma ctxt (prop, methods) =
   1.211 -  let
   1.212 -    val _ = ctxt
   1.213 -      |> Proof.theorem_i NONE (K I) [[(prop, [])]]
   1.214 -      |> Proof.global_terminal_proof methods;
   1.215 -  in pretty_term ctxt prop end;
   1.216 -
   1.217 -val embedded_lemma =
   1.218 -  args (Args.prop -- Scan.lift (Args.$$$ "by" |-- Method.parse -- Scan.option Method.parse))
   1.219 -    (output pretty_lemma o (fn ((a, arg :: _), p) => (Args.src ((a, [arg]), p))) o Args.dest_src);
   1.220 -
   1.221 -
   1.222 -(* commands *)
   1.223 +(* embedded lemma *)
   1.224  
   1.225  val _ = OuterKeyword.keyword "by";
   1.226  
   1.227 -val _ = add_commands
   1.228 - [("thm", args Attrib.thms (output_list pretty_thm)),
   1.229 -  ("thm_style", args (Scan.lift Args.liberal_name -- Attrib.thm) (output pretty_thm_style)),
   1.230 -  ("prop", args Args.prop (output pretty_term)),
   1.231 -  ("lemma", embedded_lemma),
   1.232 -  ("term", args Args.term (output pretty_term)),
   1.233 -  ("term_style", args (Scan.lift Args.liberal_name -- Args.term) (output pretty_term_style)),
   1.234 -  ("term_type", args Args.term (output pretty_term_typ)),
   1.235 -  ("typeof", args Args.term (output pretty_term_typeof)),
   1.236 -  ("const", args Args.const_proper (output pretty_const)),
   1.237 -  ("abbrev", args (Scan.lift Args.name_source) (output pretty_abbrev)),
   1.238 -  ("typ", args Args.typ_abbrev (output Syntax.pretty_typ)),
   1.239 -  ("text", args (Scan.lift Args.name) (output (K pretty_text))),
   1.240 -  ("goals", output_goals true),
   1.241 -  ("subgoals", output_goals false),
   1.242 -  ("prf", args Attrib.thms (output (pretty_prf false))),
   1.243 -  ("full_prf", args Attrib.thms (output (pretty_prf true))),
   1.244 -  ("theory", args (Scan.lift Args.name) (output pretty_theory)),
   1.245 -  ("ML", args (Scan.lift Args.name_source_position) (output_ml ml_val)),
   1.246 -  ("ML_type", args (Scan.lift Args.name_source_position) (output_ml ml_type)),
   1.247 -  ("ML_struct", args (Scan.lift Args.name_source_position) (output_ml ml_struct))];
   1.248 +val _ = antiquotation "lemma"
   1.249 +  (Args.prop -- Scan.lift (Args.$$$ "by" |-- Method.parse -- Scan.option Method.parse))
   1.250 +  (fn {source, context, ...} => fn (prop, methods) =>
   1.251 +    let
   1.252 +      val prop_src =
   1.253 +        (case Args.dest_src source of ((a, arg :: _), pos) => Args.src ((a, [arg]), pos));
   1.254 +      val _ = context
   1.255 +        |> Proof.theorem_i NONE (K I) [[(prop, [])]]
   1.256 +        |> Proof.global_terminal_proof methods;
   1.257 +    in output (maybe_pretty_source (pretty_term context) prop_src [prop]) end);
   1.258 +
   1.259 +
   1.260 +(* ML text *)
   1.261 +
   1.262 +local
   1.263 +
   1.264 +fun ml_text name ml = antiquotation name (Scan.lift Args.name_source_position)
   1.265 +  (fn {context, ...} => fn (txt, pos) =>
   1.266 +   (ML_Context.eval_in (SOME context) false pos (ml txt);
   1.267 +    SymbolPos.content (SymbolPos.explode (txt, pos))
   1.268 +    |> (if ! quotes then quote else I)
   1.269 +    |> (if ! display then enclose "\\begin{verbatim}\n" "\n\\end{verbatim}"
   1.270 +    else
   1.271 +      split_lines
   1.272 +      #> map (space_implode "\\verb,|," o map (enclose "\\verb|" "|") o space_explode "|")
   1.273 +      #> space_implode "\\isasep\\isanewline%\n")));
   1.274 +
   1.275 +in
   1.276 +
   1.277 +val _ = ml_text "ML" (fn txt => "fn _ => (" ^ txt ^ ");");
   1.278 +val _ = ml_text "ML_type" (fn txt => "val _ = NONE : (" ^ txt ^ ") option;");
   1.279 +val _ = ml_text "ML_struct"
   1.280 +  (fn txt => "functor DUMMY_FUNCTOR() = struct structure DUMMY = " ^ txt ^ " end;");
   1.281  
   1.282  end;
   1.283 +
   1.284 +end;