# HG changeset patch
# User wenzelm
# Date 1348929331 -7200
# Node ID ae8c8b745f825eaf6ca711c37bafd32d9f9d3cf2
# Parent  40e4feac2921c5eb14e0e07ecfef4b4b9515fe60
ignore wrapped markup elements in Proof General;

diff -r 40e4feac2921 -r ae8c8b745f82 src/Pure/ProofGeneral/proof_general_emacs.ML
--- a/src/Pure/ProofGeneral/proof_general_emacs.ML	Sat Sep 29 16:17:46 2012 +0200
+++ b/src/Pure/ProofGeneral/proof_general_emacs.ML	Sat Sep 29 16:35:31 2012 +0200
@@ -30,37 +30,43 @@
 local
 
 fun render_trees ts = fold render_tree ts
-and render_tree (XML.Text s) = Buffer.add s
-  | render_tree (XML.Elem ((name, props), ts)) =
-      let
-        val (bg1, en1) =
-          if name <> Isabelle_Markup.promptN andalso print_mode_active test_markupN
-          then XML.output_markup (name, props)
-          else Markup.no_output;
-        val (bg2, en2) =
-          if null ts then Markup.no_output
-          else if name = Isabelle_Markup.stateN then (special "O" ^ "\n", "\n" ^ special "P")
-          else if name = Isabelle_Markup.sendbackN then (special "W", special "X")
-          else if name = Isabelle_Markup.intensifyN then (special "0", special "1")
-          else if name = Isabelle_Markup.tfreeN then (special "C", special "A")
-          else if name = Isabelle_Markup.tvarN then (special "D", special "A")
-          else if name = Isabelle_Markup.freeN then (special "E", special "A")
-          else if name = Isabelle_Markup.boundN then (special "F", special "A")
-          else if name = Isabelle_Markup.varN then (special "G", special "A")
-          else if name = Isabelle_Markup.skolemN then (special "H", special "A")
-          else
-            (case Isabelle_Markup.get_entity_kind (name, props) of
-              SOME kind =>
-                if kind = Isabelle_Markup.classN then (special "B", special "A")
-                else Markup.no_output
-            | NONE => Markup.no_output);
-      in
-        Buffer.add bg1 #>
-        Buffer.add bg2 #>
-        render_trees ts #>
-        Buffer.add en2 #>
-        Buffer.add en1
-      end;
+
+and render_tree t =
+  (case XML.unwrap_elem t of
+    SOME (_, ts) => render_trees ts
+  | NONE =>
+      (case t of
+        XML.Text s => Buffer.add s
+      | XML.Elem ((name, props), ts) =>
+          let
+            val (bg1, en1) =
+              if name <> Isabelle_Markup.promptN andalso print_mode_active test_markupN
+              then XML.output_markup (name, props)
+              else Markup.no_output;
+            val (bg2, en2) =
+              if null ts then Markup.no_output
+              else if name = Isabelle_Markup.stateN then (special "O" ^ "\n", "\n" ^ special "P")
+              else if name = Isabelle_Markup.sendbackN then (special "W", special "X")
+              else if name = Isabelle_Markup.intensifyN then (special "0", special "1")
+              else if name = Isabelle_Markup.tfreeN then (special "C", special "A")
+              else if name = Isabelle_Markup.tvarN then (special "D", special "A")
+              else if name = Isabelle_Markup.freeN then (special "E", special "A")
+              else if name = Isabelle_Markup.boundN then (special "F", special "A")
+              else if name = Isabelle_Markup.varN then (special "G", special "A")
+              else if name = Isabelle_Markup.skolemN then (special "H", special "A")
+              else
+                (case Isabelle_Markup.get_entity_kind (name, props) of
+                  SOME kind =>
+                    if kind = Isabelle_Markup.classN then (special "B", special "A")
+                    else Markup.no_output
+                | NONE => Markup.no_output);
+          in
+            Buffer.add bg1 #>
+            Buffer.add bg2 #>
+            render_trees ts #>
+            Buffer.add en2 #>
+            Buffer.add en1
+          end));
 
 in