equal
deleted
inserted
replaced
484 |
484 |
485 |
485 |
486 fun writeTextFile name s = File.write (Path.explode name) s |
486 fun writeTextFile name s = File.write (Path.explode name) s |
487 |
487 |
488 fun use_source src = |
488 fun use_source src = |
489 ML_Compiler0.use_text ML_Env.context |
489 ML_Compiler0.ML ML_Env.context |
490 {line = 1, file = "", verbose = false, debug = false} src |
490 {line = 1, file = "", verbose = false, debug = false} src |
491 |
491 |
492 fun compile rules = |
492 fun compile rules = |
493 let |
493 let |
494 val guid = get_guid () |
494 val guid = get_guid () |