--- 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:
--- 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 *)