src/Pure/Isar/isar_cmd.ML
changeset 16258 f3d913abf7e5
parent 16193 05413e43d2f3
child 16499 2076b2e6ac58
equal deleted inserted replaced
16257:98337d5acd0e 16258:f3d913abf7e5
   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);