# HG changeset patch # User wenzelm # Date 1310729340 -7200 # Node ID 04008ec62370ea4d7927d913e2c2eb5c664d9748 # Parent 93f6f24010c252e68f7d9af7b8077f0191d215eb less ambitious ProofGeneral markup, which occasionally breaks plain-old regexps in elisp; diff -r 93f6f24010c2 -r 04008ec62370 src/Pure/ProofGeneral/proof_general_emacs.ML --- a/src/Pure/ProofGeneral/proof_general_emacs.ML Fri Jul 15 13:28:16 2011 +0200 +++ b/src/Pure/ProofGeneral/proof_general_emacs.ML Fri Jul 15 13:29:00 2011 +0200 @@ -41,7 +41,6 @@ if null ts then Markup.no_output else if name = Markup.stateN then (special "O" ^ "\n", "\n" ^ special "P") else if name = Markup.sendbackN then (special "W", special "X") - else if name = Markup.bindingN then (special "B", special "A") else if name = Markup.hiliteN then (special "0", special "1") else if name = Markup.tfreeN then (special "C", special "A") else if name = Markup.tvarN then (special "D", special "A")