1structure HOLsexp_parser :> HOLsexp_parser =
2struct
3
4  open HOLsexp_dtype
5
6  structure HOLsexpLrVals =
7    HOLsexpLrValsFun(structure Token = LrParser.Token)
8
9  structure HOLsexpLex =
10    HOLsexpLexFun(structure Tokens = HOLsexpLrVals.Tokens)
11
12
13  structure HOLsexpParser =
14     JoinWithArg(structure ParserData = HOLsexpLrVals.ParserData
15                 structure Lex = HOLsexpLex
16                 structure LrParser = LrParser)
17
18  fun invoke lexstream = let
19    fun print_error (s,i:int,_) =
20        TextIO.output(TextIO.stdErr, Int.toString i ^ ": " ^ s ^ "\n")
21  in
22    #1 (HOLsexpParser.parse(15,lexstream,print_error,ref []))
23  end
24
25  fun raw_read_stream strm = let
26    val lexer = HOLsexpParser.makeLexer
27                  (fn _ => Portable.input_line strm)
28                  (ref [] : string list ref)
29    val _ = HOLsexpLex.UserDeclarations.pos := 1
30  in
31    invoke lexer
32  end
33
34  fun raw_read_file fname = let
35    val strm = TextIO.openIn fname
36  in
37    raw_read_stream strm before TextIO.closeIn strm
38  end
39
40  fun scan creader cs =
41      let
42        val csref = ref cs
43        val lexer = HOLsexpParser.makeLexer
44                      (fn _ => case creader (!csref) of
45                                   NONE => ""
46                                 | SOME (c,cs') => (csref := cs'; str c))
47                      (ref [] : string list ref)
48        val _ = HOLsexpLex.UserDeclarations.pos := 1
49      in
50        case Exn.capture invoke lexer of
51            Exn.Res r => SOME(r, !csref)
52          | Exn.Exn e => NONE
53      end
54
55end (* struct *)
56