# 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