equal
deleted
inserted
replaced
483 end |
483 end |
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 = use_text ML_Env.local_context (1, "") false src |
488 fun use_source src = |
|
489 use_text ML_Env.local_context {line = 1, file = "", verbose = false, debug = false} src |
489 |
490 |
490 fun compile rules = |
491 fun compile rules = |
491 let |
492 let |
492 val guid = get_guid () |
493 val guid = get_guid () |
493 val code = Real.toString (Random.random ()) |
494 val code = Real.toString (Random.random ()) |