equal
deleted
inserted
replaced
107 val use_commit = use_mltext "commit();"; |
107 val use_commit = use_mltext "commit();"; |
108 |
108 |
109 |
109 |
110 (* current working directory *) |
110 (* current working directory *) |
111 |
111 |
112 fun print_cd _ = writeln (Path.pack (File.pwd ())); |
112 fun cd dir = Toplevel.imperative (fn () => (File.cd (Path.unpack dir))); |
113 |
113 val pwd = Toplevel.imperative (fn () => writeln (Path.pack (File.pwd ()))); |
114 fun cd dir = Toplevel.imperative (fn () => (File.cd (Path.unpack dir); print_cd ())); |
|
115 val pwd = Toplevel.imperative print_cd; |
|
116 |
114 |
117 |
115 |
118 (* load theory files *) |
116 (* load theory files *) |
119 |
117 |
120 fun use_thy name = Toplevel.imperative (fn () => Context.save ThyInfo.use_thy name); |
118 fun use_thy name = Toplevel.imperative (fn () => Context.save ThyInfo.use_thy name); |