src/Pure/proof_general.ML
changeset 15403 9e58e666074d
parent 15401 ba28d103bada
child 15457 1fbd4aba46e3
     1.1 --- a/src/Pure/proof_general.ML	Sun Dec 12 16:25:47 2004 +0100
     1.2 +++ b/src/Pure/proof_general.ML	Mon Dec 13 14:31:02 2004 +0100
     1.3 @@ -90,8 +90,8 @@
     1.4      (* NB: an alternative here would be to output the default print mode alternative
     1.5         in the element content, but unfortunately print modes are not that fine grained. *)
     1.6      Symbol.Char s => XML.text s
     1.7 -  | Symbol.Sym s => XML.element "sym" [("name", s)] [XML.text s]
     1.8 -  | Symbol.Ctrl s => XML.element "ctrl" [("name", s)] []  (* FIXME: no such PGML! *)
     1.9 +  | Symbol.Sym sn => XML.element "sym" [("name", sn)] [XML.text s]
    1.10 +  | Symbol.Ctrl sn => XML.element "ctrl" [("name", sn)] [XML.text s]   (* FIXME: no such PGML! *)
    1.11    | Symbol.Raw s => s);
    1.12  
    1.13  fun pgml_output str =
    1.14 @@ -1154,10 +1154,8 @@
    1.15       | "proverexit" 	=> isarcmd "quit"
    1.16       | "startquiet" 	=> isarcmd "disable_pr"
    1.17       | "stopquiet"  	=> isarcmd "enable_pr"
    1.18 -     | "pgmlsymbolson"   => (print_mode := (["xsymbols", "symbols"] @ ! print_mode))
    1.19 -     | "pgmlsymbolsoff"  => (print_mode := (Library.gen_rems 
    1.20 -						(op =) 
    1.21 -						(! print_mode, ["xsymbols", "symbols"])))
    1.22 +     | "pgmlsymbolson"   => (print_mode := !print_mode @ ["xsymbols"])
    1.23 +     | "pgmlsymbolsoff"  => (print_mode := (!print_mode \ "xsymbols"))
    1.24       (* properproofcmd: proper commands which belong in script *)
    1.25       (* FIXME: next ten are by Eclipse interface, can be removed in favour of dostep *)
    1.26       | "opengoal"       => isarscript data