equal
deleted
inserted
replaced
15 (* re-definition of various ML antiquotations *) |
15 (* re-definition of various ML antiquotations *) |
16 (* to have a special tag for text enclosed in ML *) |
16 (* to have a special tag for text enclosed in ML *) |
17 |
17 |
18 ML {* |
18 ML {* |
19 (* FIXME ref *) |
19 (* FIXME ref *) |
20 val file_name = ref (NONE : string option) |
20 val file_name = Unsynchronized.ref (NONE : string option) |
21 |
21 |
22 fun write_file txt = |
22 fun write_file txt = |
23 case !file_name of |
23 case !file_name of |
24 NONE => () (* error "No open file" *) |
24 NONE => () (* error "No open file" *) |
25 | SOME name => |
25 | SOME name => |