1open testutils 2 3infix ++ 4fun p1 ++ p2 = OS.Path.concat(p1,p2) 5 6val _ = tprint "Checking holpathdb bindings make it into interactive sessions" 7 8val _ = Systeml.system_ps (Globals.HOLDIR ++ "bin" ++ "hol.bare" ^ " < input > /dev/null 2>&1") 9 10exception InternalDie of string 11 12val _ = let 13 val istrmr = Exn.capture TextIO.openIn "output" 14 val istrm = case istrmr of 15 Res i => i 16 | Exn e => raise InternalDie 17 ("Exception: "^General.exnMessage e) 18in 19 case TextIO.inputLine istrm of 20 SOME s => 21 if String.isSubstring "tools/Holmake/tests/holpathdb/proj2" s then 22 OK() 23 else die ("Saw:\n "^ s) 24 | NONE => die "Nothing in \"output\"" 25end handle InternalDie s => die s; 26