Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Revert change to pgml_sym
authoraspinall
Wed, 27 Oct 2004 19:45:16 +0200
changeset 15266 0398af5501fe
parent 15265 a1547232fedd
child 15267 96c59666a0bf
Revert change to pgml_sym
src/Pure/proof_general.ML file | annotate | diff | comparison | revisions 
--- a/src/Pure/proof_general.ML	Wed Oct 27 10:30:07 2004 +0200
+++ b/src/Pure/proof_general.ML	Wed Oct 27 19:45:16 2004 +0200
@@ -89,8 +89,10 @@
   (case Symbol.decode s of
     (* NB: an alternative here would be to output the default print mode alternative
        in the element content, but unfortunately print modes are not that fine grained. *)
-    Symbol.Sym s => XML.element "sym" [("name", s)] [XML.text s]
-  | _ => XML.text s)
+    Symbol.Char s => XML.text s
+  | Symbol.Sym s => XML.element "sym" [("name", s)] [XML.text s]
+  | Symbol.Ctrl s => XML.element "ctrl" [("name", s)] []  (* FIXME: no such PGML! *)
+  | Symbol.Raw s => s);
 
 fun pgml_output str =
   let val syms = Symbol.explode str
isabelle