equal
deleted
inserted
replaced
186 |
186 |
187 |
187 |
188 (* present draft files *) |
188 (* present draft files *) |
189 |
189 |
190 fun display_drafts files = Toplevel.imperative (fn () => |
190 fun display_drafts files = Toplevel.imperative (fn () => |
191 let val outfile = File.quote_sysify_path (Present.drafts (getenv "ISABELLE_DOC_FORMAT") files) |
191 let val outfile = File.shell_path (Present.drafts (getenv "ISABELLE_DOC_FORMAT") files) |
192 in system ("\"$ISATOOL\" display -c " ^ outfile ^ " &"); () end); |
192 in File.isatool ("display -c " ^ outfile ^ " &"); () end); |
193 |
193 |
194 fun print_drafts files = Toplevel.imperative (fn () => |
194 fun print_drafts files = Toplevel.imperative (fn () => |
195 let val outfile = File.quote_sysify_path (Present.drafts "ps" files) |
195 let val outfile = File.shell_path (Present.drafts "ps" files) |
196 in system ("\"$ISATOOL\" print -c " ^ outfile); () end); |
196 in File.isatool ("print -c " ^ outfile); () end); |
197 |
197 |
198 |
198 |
199 (* pretty_setmargin *) |
199 (* pretty_setmargin *) |
200 |
200 |
201 fun pretty_setmargin n = Toplevel.imperative (fn () => Pretty.setmargin n); |
201 fun pretty_setmargin n = Toplevel.imperative (fn () => Pretty.setmargin n); |