# HG changeset patch # User Christian Urban # Date 1233851645 0 # Node ID 018bfa71898209d70789ad3c217605b2f65eac0f # Parent 7235374f34c85b66073b5bac0663fab74ace7c67 (re)defined the document antiquotation @subgoal in order to be closer to what is actually printed diff -r 7235374f34c8 -r 018bfa718982 CookBook/antiquote_setup.ML --- a/CookBook/antiquote_setup.ML Wed Feb 04 20:26:38 2009 +0000 +++ b/CookBook/antiquote_setup.ML Thu Feb 05 16:34:05 2009 +0000 @@ -57,6 +57,27 @@ if File.exists (Path.append (Path.explode ("~~/src")) (Path.explode txt)) then () else error ("Source file " ^ quote txt ^ " does not exist.") +(* to be closer to the actual output *) +fun output_goals main_goal src node = +let + fun subgoals 0 = "No subgoals!" + | subgoals 1 = "goal (1 subgoal):" + | subgoals n = "goal (" ^ string_of_int n ^ " subgoals):"; + + fun proof_state node = + (case Option.map Toplevel.proof_node node of + SOME (SOME prf) => ProofNode.current prf + | _ => error "No proof state"); + + val state = proof_state node + val goals = Proof.pretty_goals main_goal state; + val msg = Pretty.str (subgoals (length goals)) +in + ThyOutput.args (Scan.succeed ()) + (Chunks.output (fn _ => fn _ => Pretty.chunks (msg::goals))) src node +end + + val _ = ThyOutput.add_commands [("ML", ThyOutput.args (Scan.lift (OuterParse.position (Args.name -- (Scan.optional (Args.$$$ "for" |-- OuterParse.!!! (Scan.repeat1 Args.name)) [] -- @@ -73,6 +94,7 @@ ("ML_response_fake_both", ThyOutput.args (Scan.lift (OuterParse.position (Args.name -- Args.name))) (output_ml_response_fake_both ml_val)), ("ML_struct", ThyOutput.args (Scan.lift (OuterParse.position Args.name)) (output_ml_aux ml_struct)), - ("ML_type", ThyOutput.args (Scan.lift (OuterParse.position Args.name)) (output_ml_aux ml_type))]; + ("ML_type", ThyOutput.args (Scan.lift (OuterParse.position Args.name)) (output_ml_aux ml_type)), + ("subgoals", output_goals false)]; end; diff -r 7235374f34c8 -r 018bfa718982 CookBook/chunks.ML --- a/CookBook/chunks.ML Wed Feb 04 20:26:38 2009 +0000 +++ b/CookBook/chunks.ML Thu Feb 05 16:34:05 2009 +0000 @@ -26,9 +26,14 @@ #> space_implode "\\isasep\\isanewline%\n" #> enclose "\\isa{" "}"); +fun output pretty src ctxt = output_list pretty src ctxt o single + val _ = ThyOutput.add_options [("gray", Library.setmp gray o boolean)] + + + (** theory data **) structure ChunkData = TheoryDataFun