# HG changeset patch
# User aspinall
# Date 1098625312 -7200
# Node ID 10cfd6a146821c76d6cd359d5bb3761e3b55d2e7
# Parent  6e20cc79bde68b6cf8f27d2071622981a52faed0
Simplification to symbol processing; put quotes around theory name in message.

diff -r 6e20cc79bde6 -r 10cfd6a14682 src/Pure/proof_general.ML
--- a/src/Pure/proof_general.ML	Thu Oct 21 19:21:32 2004 +0200
+++ b/src/Pure/proof_general.ML	Sun Oct 24 15:41:52 2004 +0200
@@ -87,10 +87,10 @@
 
 fun pgml_sym s =
   (case Symbol.decode s of
-    Symbol.Char s => XML.text s
-  | Symbol.Sym s => XML.element "sym" [("name", s)] []
-  | Symbol.Ctrl s => XML.element "ctrl" [("name", s)] []
-  | Symbol.Raw s => s);
+    (* 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)
 
 fun pgml_output str =
   let val syms = Symbol.explode str
@@ -712,12 +712,11 @@
    was removed during parsing so we can provide markup around commands;
    2) parsing is intertwined with execution in Isar so we have to repeat
    the parsing to extract interesting parts of commands.  The trace of
-   tokens parsed which is now recorded in each transition helps do this.
+   tokens parsed which is now recorded in each transition (added by
+   Markus June '04) helps do this, but the mechanism is still a bad mess.
    
-   If we had proper parse trees it would be easy, or if we could go
-   beyond ML's type system to allow existential types to be part of
-   parsers (the quantified type representing the result of the parse
-   which is used to make the transition function) it might be possible.
+   If we had proper parse trees it would be easy, although having a
+   fixed type of trees might be tricky with Isar's extensible parser.
 
    Probably the best solution is to produce the meta-information at
    the same time as the parse, for each command, e.g. by recording a 
@@ -731,6 +730,15 @@
       (token list -> 
        ((Toplevel.transition -> Toplevel.transition) * metainfo list) * 
        token list) -> parser
+
+   We'd also like to render terms as they appear in output, but this
+   will be difficult because inner syntax is extensible and we don't 
+   have the correct syntax to hand when just doing outer parsing
+   without execution.  A reasonable approximation could 
+   perhaps be obtained by using the syntax of the current context.
+   However, this would mean more mess trying to pick out terms, 
+   so at this stage a more serious change to the Isar functions
+   seems necessary.
 *)
 
 local
@@ -820,6 +828,12 @@
 		    theoremsP
 		end
 	in 
+	    (* TODO: ideally we would like to render terms properly, just as they are
+	       in output. This implies using PGML for symbols and variables/atoms. 
+	       BUT it's rather tricky without having the correct concrete syntax to hand,
+	       and even if we did, we'd have to mess around here a whole lot more first
+	       to pick out the terms from the syntax. *)
+
 	    if (name mem plain_items) then plain_item
 	    else case name of
 		     "text"      => comment_item
@@ -1171,7 +1185,7 @@
      | "closetheory"    => let 
 			      val thyname = topthy_name()
 			   in (isarscript data;
-			       writeln ("Theory "^thyname^" completed."))
+			       writeln ("Theory \""^thyname^"\" completed."))
 			   end
      (* improperfilecmd: theory-level commands not in script *)
      | "aborttheory"    => isarcmd ("init_toplevel")