equal
deleted
inserted
replaced
55 fun init proof_file _ thy = |
55 fun init proof_file _ thy = |
56 let |
56 let |
57 fun do_line line = |
57 fun do_line line = |
58 (case line |> space_explode ":" of |
58 (case line |> space_explode ":" of |
59 [line_num, offset, proof] => |
59 [line_num, offset, proof] => |
60 SOME (pairself (the o Int.fromString) (line_num, offset), |
60 SOME (apply2 (the o Int.fromString) (line_num, offset), |
61 proof |> space_explode " " |> filter_out (curry (op =) "")) |
61 proof |> space_explode " " |> filter_out (curry (op =) "")) |
62 | _ => NONE) |
62 | _ => NONE) |
63 val proofs = File.read (Path.explode proof_file) |
63 val proofs = File.read (Path.explode proof_file) |
64 val proof_tab = |
64 val proof_tab = |
65 proofs |> space_explode "\n" |
65 proofs |> space_explode "\n" |