src/Pure/Isar/isar_cmd.ML
changeset 14934 bf9f525d4821
parent 13801 6c5c5bdfae84
child 14950 e22fad2b6f6f
equal deleted inserted replaced
14933:3fd8c03e3ee6 14934:bf9f525d4821
    38   val pwd: Toplevel.transition -> Toplevel.transition
    38   val pwd: Toplevel.transition -> Toplevel.transition
    39   val use_thy: string -> Toplevel.transition -> Toplevel.transition
    39   val use_thy: string -> Toplevel.transition -> Toplevel.transition
    40   val use_thy_only: string -> Toplevel.transition -> Toplevel.transition
    40   val use_thy_only: string -> Toplevel.transition -> Toplevel.transition
    41   val update_thy: string -> Toplevel.transition -> Toplevel.transition
    41   val update_thy: string -> Toplevel.transition -> Toplevel.transition
    42   val update_thy_only: string -> Toplevel.transition -> Toplevel.transition
    42   val update_thy_only: string -> Toplevel.transition -> Toplevel.transition
       
    43   val display_drafts: string list -> Toplevel.transition -> Toplevel.transition
       
    44   val print_drafts: string list -> Toplevel.transition -> Toplevel.transition
    43   val pretty_setmargin: int -> Toplevel.transition -> Toplevel.transition
    45   val pretty_setmargin: int -> Toplevel.transition -> Toplevel.transition
    44   val print_context: Toplevel.transition -> Toplevel.transition
    46   val print_context: Toplevel.transition -> Toplevel.transition
    45   val print_theory: Toplevel.transition -> Toplevel.transition
    47   val print_theory: Toplevel.transition -> Toplevel.transition
    46   val print_syntax: Toplevel.transition -> Toplevel.transition
    48   val print_syntax: Toplevel.transition -> Toplevel.transition
    47   val print_theorems: Toplevel.transition -> Toplevel.transition
    49   val print_theorems: Toplevel.transition -> Toplevel.transition
   177 fun update_thy name = Toplevel.imperative (fn () => Context.save ThyInfo.update_thy name);
   179 fun update_thy name = Toplevel.imperative (fn () => Context.save ThyInfo.update_thy name);
   178 fun update_thy_only name =
   180 fun update_thy_only name =
   179   Toplevel.imperative (fn () => Context.save ThyInfo.update_thy_only name);
   181   Toplevel.imperative (fn () => Context.save ThyInfo.update_thy_only name);
   180 
   182 
   181 
   183 
       
   184 (* present draft files *)
       
   185 
       
   186 fun display_drafts files = Toplevel.imperative (fn () =>
       
   187   let val outfile = File.quote_sysify_path (Present.drafts "dvi" (map Path.unpack files))
       
   188   in system ("\"$ISATOOL\" display -c " ^ outfile ^ " &"); () end);
       
   189 
       
   190 fun print_drafts files = Toplevel.imperative (fn () =>
       
   191   let val outfile = File.quote_sysify_path (Present.drafts "ps" (map Path.unpack files))
       
   192   in system ("\"$ISATOOL\" print -c " ^ outfile); () end);
       
   193 
       
   194 
   182 (* pretty_setmargin *)
   195 (* pretty_setmargin *)
   183 
   196 
   184 fun pretty_setmargin n = Toplevel.imperative (fn () => Pretty.setmargin n);
   197 fun pretty_setmargin n = Toplevel.imperative (fn () => Pretty.setmargin n);
   185 
   198 
   186 
   199