src/Pure/Isar/isar_cmd.ML
changeset 7124 78c01842d3b5
parent 7101 ee79bf6feee2
child 7308 e01aab03a2a1
     1.1 --- a/src/Pure/Isar/isar_cmd.ML	Wed Jul 28 13:55:34 1999 +0200
     1.2 +++ b/src/Pure/Isar/isar_cmd.ML	Wed Jul 28 18:55:35 1999 +0200
     1.3 @@ -31,6 +31,7 @@
     1.4    val use_thy_only: string -> Toplevel.transition -> Toplevel.transition
     1.5    val update_thy: string -> Toplevel.transition -> Toplevel.transition
     1.6    val update_thy_only: string -> Toplevel.transition -> Toplevel.transition
     1.7 +  val pretty_setmargin: int -> Toplevel.transition -> Toplevel.transition
     1.8    val print_theory: Toplevel.transition -> Toplevel.transition
     1.9    val print_syntax: Toplevel.transition -> Toplevel.transition
    1.10    val print_theorems: Toplevel.transition -> Toplevel.transition
    1.11 @@ -117,7 +118,13 @@
    1.12  fun use_thy name = Toplevel.imperative (fn () => Context.save ThyInfo.use_thy name);
    1.13  fun use_thy_only name = Toplevel.imperative (fn () => Context.save ThyInfo.use_thy_only name);
    1.14  fun update_thy name = Toplevel.imperative (fn () => Context.save ThyInfo.update_thy name);
    1.15 -fun update_thy_only name = Toplevel.imperative (fn () => Context.save ThyInfo.update_thy_only name);
    1.16 +fun update_thy_only name =
    1.17 +  Toplevel.imperative (fn () => Context.save ThyInfo.update_thy_only name);
    1.18 +
    1.19 +
    1.20 +(* pretty_setmargin *)
    1.21 +
    1.22 +fun pretty_setmargin n = Toplevel.imperative (fn () => Pretty.setmargin n);
    1.23  
    1.24  
    1.25  (* print theory contents *)