# HG changeset patch
# User aspinall
# Date 1169476618 -3600
# Node ID 27cdecde8c2b5f2929f05d93d272c91896953b43
# Parent  0cf0d3912239c3776d71db3a2625546a7cd4c54b
Comments

diff -r 0cf0d3912239 -r 27cdecde8c2b src/Pure/ProofGeneral/README
--- a/src/Pure/ProofGeneral/README	Mon Jan 22 15:34:15 2007 +0100
+++ b/src/Pure/ProofGeneral/README	Mon Jan 22 15:36:58 2007 +0100
@@ -14,19 +14,19 @@
 The code constructs some marshalling datatypes for reading and writing
 XML which conforms to the PGIP schema, interfacing with SML types and
 some basic types from the Isabelle platform (i.e. URLs, XML).  This
-part of the code is intended to be useful for reuse or porting
-elsewhere, so it should have minimal dependency on Isabelle and be
-written readably.  Some languages have tools for making type-safe
-XML<->native datatype translations from a schema (e.g. HaXML for
-Haskell) which would be useful here.
+portion is intended to be useful for reuse or porting elsewhere, so it
+should have minimal dependency on Isabelle and be written readably.
+Some languages have tools for making type-safe XML<->native datatype
+translations from a schema (e.g. HaXML for Haskell) which would be
+useful here.
 
 The Isabelle specific configuration is in these files:
 
-  pgip_isabelle.ML	  - configure part of PGIP supported by Isabelle
-  parsing.ML		  - parsing routines to add PGIP markup to scripts
-  preferences.ML	  - user preferences
-  proof_general_pgip.ML   - the main connection point with Isabelle, including
-			    the PGIP processing loop.
+  pgip_isabelle.ML	 - configure part of PGIP supported by Isabelle + type mapping
+  parsing.ML		 - parsing routines to add PGIP markup to scripts
+  preferences.ML	 - user preferences
+  proof_general_pgip.ML  - the main connection point with Isabelle, including
+			   the PGIP processing loop.
 
 For the full PGIP schema and an explanation of it, see:
 
diff -r 0cf0d3912239 -r 27cdecde8c2b src/Pure/ProofGeneral/parsing.ML
--- a/src/Pure/ProofGeneral/parsing.ML	Mon Jan 22 15:34:15 2007 +0100
+++ b/src/Pure/ProofGeneral/parsing.ML	Mon Jan 22 15:36:58 2007 +0100
@@ -246,8 +246,10 @@
            [D.Theoryitem {name=NONE,objtype=NONE,text=str}])
    end
 
+
+(* this would be a lot neater if we could match on toks! *)
 fun markup_comment_whs [] = []
-  | markup_comment_whs (toks as t::ts) = (* this would be a lot neater if we could match on toks! *)
+  | markup_comment_whs (toks as t::ts) = 
     let
         val (prewhs,rest) = take_prefix (OuterLex.is_kind OuterLex.Space) toks
     in
@@ -320,8 +322,9 @@
            let
                (* first proper token after whitespace/litcomment/whitespace is command *)
                val (xmls_pre_cmd,cmditoks') = xmls_pre_cmd itoks
-               val (cmdtok,itoks') = case cmditoks' of x::xs => (x,xs)
-                                                     | _ => error("proof_general/parse_loop impossible")
+               val (cmdtok,itoks') = 
+		   case cmditoks' of x::xs => (x,xs)
+                                   | _ => error("proof_general/parse_loop impossible")
                val (utoks,itoks'') = match_tokens (toks,itoks',[])
                (* FIXME: should take trailing [w/s+] semicolon too in utoks *)