update other files using b_input

examples/eval/eval_exampleProgScript.sml

@@ -28,13 +28,14 @@ End
 
 val res = translate trimr_def;
 
+(* TODO changed but this file is broken *)
 val fname_to_words = process_topdecs`
   fun fname_to_words from_int fname =
     List.map
       (from_int o
        Option.valOf o Int.fromNatString o
        trimr)
-      (Option.valOf (TextIO.b_inputLinesFrom fname))
+      (Option.valOf (TextIO.b_inputLinesFrom #"\n" fname))
     handle _ => (print "Error reading data to eval.\n";
                  Runtime.exit 1; [])`;
 

examples/opentheory/readerProgScript.sml

@@ -267,7 +267,7 @@ val _ = (append_prog o process_topdecs) `
 
 val _ = (append_prog o process_topdecs) `
   fun read_file file =
-    case TextIO.b_inputAllTokensFrom file is_newline tokenize of
+    case TextIO.b_inputAllTokensFrom #"\n" file is_newline tokenize of
       None =>
         TextIO.output TextIO.stdErr (msg_bad_name file)
     | Some ls =>
@@ -366,7 +366,7 @@ Theorem b_inputAllTokensFrom_spec2:
   FILENAME fn fnv ∧
   hasFreeFD fs ⇒
     app (p: 'ffi ffi_proj) TextIO_b_inputAllTokensFrom_v
-      [fnv; is_newline_v; tokenize_v]
+      [Litv (Char #"\n") ; fnv; is_newline_v; tokenize_v]
       (STDIO fs)
       (POSTv sv.
         &OPTION_TYPE (LIST_TYPE (LIST_TYPE READER_COMMAND_TYPE))
@@ -378,6 +378,9 @@ Theorem b_inputAllTokensFrom_spec2:
         STDIO fs)
 Proof
   strip_tac
+  \\ `all_lines fs fn = all_lines_gen #"\n" fs fn` by
+    rw[all_lines_def,all_lines_gen_def,lines_of_def,lines_of_gen_def,splitlines_at_def,splitlines_def,str_def]
+  \\ pop_assum SUBST_ALL_TAC
   \\ irule b_inputAllTokensFrom_spec
   \\ simp [theorem "is_newline_v_thm", tokenize_v_thm, is_newline_def]
 QED