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