markup binding like class, which is the only special markup where Proof General (including version 4.1) allows "isar-long-id-stuff";
1.1 --- a/src/Pure/ProofGeneral/proof_general_emacs.ML Mon Jun 27 09:42:46 2011 +0200
1.2 +++ b/src/Pure/ProofGeneral/proof_general_emacs.ML Mon Jun 27 14:38:58 2011 +0200
1.3 @@ -41,7 +41,7 @@
1.4 if null ts then Markup.no_output
1.5 else if name = Markup.stateN then (special "O" ^ "\n", "\n" ^ special "P")
1.6 else if name = Markup.sendbackN then (special "W", special "X")
1.7 - else if name = Markup.bindingN then (special "F", special "A")
1.8 + else if name = Markup.bindingN then (special "B", special "A")
1.9 else if name = Markup.hiliteN then (special "0", special "1")
1.10 else if name = Markup.tfreeN then (special "C", special "A")
1.11 else if name = Markup.tvarN then (special "D", special "A")