New and improved HOL parser

Manual/Tools/polyscripter.sml

@@ -17,11 +17,11 @@ fun lnumdie linenum extra exn =
 
 val outputPrompt = ref "> "
 
-val quote = QFRead.fromString
+val quote = HolParser.fromString
 val default_linewidth = 77
 
 fun quoteFile lnum fname =
-  QFRead.inputFile fname handle e => lnumdie lnum "" e
+  HolParser.inputFile fname handle e => lnumdie lnum "" e
 
 datatype lbuf =
          LB of {
@@ -319,7 +319,7 @@ fun process_line debugp umap obuf origline lbuf = let
     end
   val assertcmd = "##assert "
   val assertcmdsz = size assertcmd
-  val stringCReader = #read o QFRead.stringToReader true
+  val stringCReader = #read o HolParser.stringToReader true
   fun compile exnhandle input =
       (if debugp then
          TextIO.output(TextIO.stdErr, input)

developers/genUseScript.sml

@@ -39,9 +39,9 @@ in
   (push, read, reset)
 end;
 
-val _ = use "../tools/Holmake/QuoteFilter.sml";
-val _ = use "../tools/Holmake/QFRead.sig";
-val _ = use "../tools/Holmake/QFRead.sml";
+val _ = use "../tools/Holmake/HolLex.sml";
+val _ = use "../tools/Holmake/HolParser.sig";
+val _ = use "../tools/Holmake/HolParser.sml";
 val _ = use "../tools/Holmake/Holdep_tokens.sig"
 val _ = use "../tools/Holmake/Holdep_tokens.sml";
 

src/AI/sml_inspection/smlExecute.sml

@@ -29,7 +29,7 @@ val sml_thml_glob = ref []
 
 fun quse_string s =
   let
-    val stream = TextIO.openString (QFRead.fromString false s)
+    val stream = TextIO.openString (HolParser.fromString false s)
     fun infn () = TextIO.input1 stream
   in
     (