# HG changeset patch
# User wenzelm
# Date 1330443812 -3600
# Node ID 85f8e39327126fb7dc00af24836a938baabea0ac
# Parent  0162a0d284ac1598ba8b7f4e30d90260023438e7
display proof results as "state", to suppress odd squiggles in the Prover IDE (see also 9240be8c8c69);

diff -r 0162a0d284ac -r 85f8e3932712 src/Pure/Isar/element.ML
--- a/src/Pure/Isar/element.ML	Tue Feb 28 14:24:37 2012 +0100
+++ b/src/Pure/Isar/element.ML	Tue Feb 28 16:43:32 2012 +0100
@@ -287,8 +287,8 @@
 
 fun proof_local cmd goal_ctxt int after_qed' propss =
   Proof.map_context (K goal_ctxt) #>
-  Proof.local_goal (Proof_Display.print_results int) (K I) Proof_Context.bind_propp_i
-    cmd NONE after_qed' (map (pair Thm.empty_binding) propss);
+  Proof.local_goal (Proof_Display.print_results Isabelle_Markup.state int) (K I)
+    Proof_Context.bind_propp_i cmd NONE after_qed' (map (pair Thm.empty_binding) propss);
 
 in
 
diff -r 0162a0d284ac -r 85f8e3932712 src/Pure/Isar/obtain.ML
--- a/src/Pure/Isar/obtain.ML	Tue Feb 28 14:24:37 2012 +0100
+++ b/src/Pure/Isar/obtain.ML	Tue Feb 28 16:43:32 2012 +0100
@@ -299,7 +299,7 @@
 
     val goal = Var (("guess", 0), propT);
     fun print_result ctxt' (k, [(s, [_, th])]) =
-      Proof_Display.print_results int ctxt' (k, [(s, [th])]);
+      Proof_Display.print_results Isabelle_Markup.state int ctxt' (k, [(s, [th])]);
     val before_qed = SOME (Method.primitive_text (Goal.conclude #> Raw_Simplifier.norm_hhf #>
         (fn th => Goal.protect (Conjunction.intr (Drule.mk_term (Thm.cprop_of th)) th))));
     fun after_qed [[_, res]] =
diff -r 0162a0d284ac -r 85f8e3932712 src/Pure/Isar/proof.ML
--- a/src/Pure/Isar/proof.ML	Tue Feb 28 14:24:37 2012 +0100
+++ b/src/Pure/Isar/proof.ML	Tue Feb 28 16:43:32 2012 +0100
@@ -991,7 +991,8 @@
 local
 
 fun gen_have prep_att prepp before_qed after_qed stmt int =
-  local_goal (Proof_Display.print_results int) prep_att prepp "have" before_qed after_qed stmt;
+  local_goal (Proof_Display.print_results Isabelle_Markup.state int)
+    prep_att prepp "have" before_qed after_qed stmt;
 
 fun gen_show prep_att prepp before_qed after_qed stmt int state =
   let
@@ -1003,7 +1004,8 @@
       |> cat_lines;
 
     fun print_results ctxt res =
-      if ! testing then () else Proof_Display.print_results int ctxt res;
+      if ! testing then ()
+      else Proof_Display.print_results Isabelle_Markup.state int ctxt res;
     fun print_rule ctxt th =
       if ! testing then rule := SOME th
       else if int then
diff -r 0162a0d284ac -r 85f8e3932712 src/Pure/Isar/proof_display.ML
--- a/src/Pure/Isar/proof_display.ML	Tue Feb 28 14:24:37 2012 +0100
+++ b/src/Pure/Isar/proof_display.ML	Tue Feb 28 16:43:32 2012 +0100
@@ -17,7 +17,8 @@
   val pretty_full_theory: bool -> theory -> Pretty.T
   val print_theory: theory -> unit
   val string_of_rule: Proof.context -> string -> thm -> string
-  val print_results: bool -> Proof.context -> ((string * string) * (string * thm list) list) -> unit
+  val print_results: Markup.T -> bool -> Proof.context ->
+    ((string * string) * (string * thm list) list) -> unit
   val print_consts: bool -> Proof.context -> (string * typ -> bool) -> (string * typ) list -> unit
 end
 
@@ -100,16 +101,18 @@
 
 in
 
-fun print_results do_print ctxt ((kind, name), facts) =
+fun print_results markup do_print ctxt ((kind, name), facts) =
   if not do_print orelse kind = "" then ()
   else if name = "" then
-    Pretty.writeln (Pretty.block (Pretty.command kind :: Pretty.brk 1 :: pretty_facts ctxt facts))
-  else Pretty.writeln
-    (case facts of
-      [fact] => Pretty.blk (1, [pretty_fact_name (kind, name), Pretty.fbrk,
-        Proof_Context.pretty_fact_aux ctxt false fact])
-    | _ => Pretty.blk (1, [pretty_fact_name (kind, name), Pretty.fbrk,
-        Pretty.blk (1, Pretty.str "(" :: pretty_facts ctxt facts @ [Pretty.str ")"])]));
+    (Pretty.writeln o Pretty.mark markup)
+      (Pretty.block (Pretty.command kind :: Pretty.brk 1 :: pretty_facts ctxt facts))
+  else
+    (Pretty.writeln o Pretty.mark markup)
+      (case facts of
+        [fact] => Pretty.blk (1, [pretty_fact_name (kind, name), Pretty.fbrk,
+          Proof_Context.pretty_fact_aux ctxt false fact])
+      | _ => Pretty.blk (1, [pretty_fact_name (kind, name), Pretty.fbrk,
+          Pretty.blk (1, Pretty.str "(" :: pretty_facts ctxt facts @ [Pretty.str ")"])]));
 
 end;
 
diff -r 0162a0d284ac -r 85f8e3932712 src/Pure/Isar/specification.ML
--- a/src/Pure/Isar/specification.ML	Tue Feb 28 14:24:37 2012 +0100
+++ b/src/Pure/Isar/specification.ML	Tue Feb 28 16:43:32 2012 +0100
@@ -300,7 +300,7 @@
       |> Attrib.partial_evaluation ctxt'
       |> Element.transform_facts (Proof_Context.export_morphism ctxt' lthy);
     val (res, lthy') = lthy |> Local_Theory.notes_kind kind facts';
-    val _ = Proof_Display.print_results int lthy' ((kind, ""), res);
+    val _ = Proof_Display.print_results Markup.empty int lthy' ((kind, ""), res);
   in (res, lthy') end;
 
 in
@@ -399,12 +399,12 @@
               (map2 (fn (b, _) => fn ths => (b, [(ths, [])])) stmt results') lthy;
         val lthy'' =
           if Attrib.is_empty_binding (name, atts) then
-            (Proof_Display.print_results int lthy' ((kind, ""), res); lthy')
+            (Proof_Display.print_results Markup.empty int lthy' ((kind, ""), res); lthy')
           else
             let
               val ([(res_name, _)], lthy'') =
                 Local_Theory.notes_kind kind [((name, atts), [(maps #2 res, [])])] lthy';
-              val _ = Proof_Display.print_results int lthy' ((kind, res_name), res);
+              val _ = Proof_Display.print_results Markup.empty int lthy' ((kind, res_name), res);
             in lthy'' end;
       in after_qed results' lthy'' end;
   in