# HG changeset patch
# User wenzelm
# Date 933180935 -7200
# Node ID 78c01842d3b5e1e090391cc529899df391014e27
# Parent  4ab38de3fd200a9fd23b66514d82f5e24338dd66
added pretty_setmargin;

diff -r 4ab38de3fd20 -r 78c01842d3b5 src/Pure/Isar/isar_cmd.ML
--- a/src/Pure/Isar/isar_cmd.ML	Wed Jul 28 13:55:34 1999 +0200
+++ b/src/Pure/Isar/isar_cmd.ML	Wed Jul 28 18:55:35 1999 +0200
@@ -31,6 +31,7 @@
   val use_thy_only: string -> Toplevel.transition -> Toplevel.transition
   val update_thy: string -> Toplevel.transition -> Toplevel.transition
   val update_thy_only: string -> Toplevel.transition -> Toplevel.transition
+  val pretty_setmargin: int -> Toplevel.transition -> Toplevel.transition
   val print_theory: Toplevel.transition -> Toplevel.transition
   val print_syntax: Toplevel.transition -> Toplevel.transition
   val print_theorems: Toplevel.transition -> Toplevel.transition
@@ -117,7 +118,13 @@
 fun use_thy name = Toplevel.imperative (fn () => Context.save ThyInfo.use_thy name);
 fun use_thy_only name = Toplevel.imperative (fn () => Context.save ThyInfo.use_thy_only name);
 fun update_thy name = Toplevel.imperative (fn () => Context.save ThyInfo.update_thy name);
-fun update_thy_only name = Toplevel.imperative (fn () => Context.save ThyInfo.update_thy_only name);
+fun update_thy_only name =
+  Toplevel.imperative (fn () => Context.save ThyInfo.update_thy_only name);
+
+
+(* pretty_setmargin *)
+
+fun pretty_setmargin n = Toplevel.imperative (fn () => Pretty.setmargin n);
 
 
 (* print theory contents *)
diff -r 4ab38de3fd20 -r 78c01842d3b5 src/Pure/Isar/isar_syn.ML
--- a/src/Pure/Isar/isar_syn.ML	Wed Jul 28 13:55:34 1999 +0200
+++ b/src/Pure/Isar/isar_syn.ML	Wed Jul 28 18:55:35 1999 +0200
@@ -426,6 +426,10 @@
 
 (** diagnostic commands (for interactive mode only) **)
 
+val pretty_setmarginP =
+  OuterSyntax.improper_command "pretty_setmargin" "change default margin for pretty printing"
+    K.diag (P.nat >> IsarCmd.pretty_setmargin);
+
 val print_commandsP =
   OuterSyntax.improper_command "help" "print outer syntax (global)" K.diag
     (Scan.succeed (Toplevel.imperative OuterSyntax.print_outer_syntax));
@@ -567,9 +571,9 @@
   skip_proofP, applyP, then_applyP, proofP, alsoP, finallyP, backP,
   cannot_undoP, clear_undoP, redoP, undos_proofP, kill_proofP, undoP,
   (*diagnostic commands*)
-  print_commandsP, print_theoryP, print_syntaxP, print_attributesP,
-  print_methodsP, print_theoremsP, print_bindsP, print_lthmsP,
-  print_thmsP, print_propP, print_termP, print_typeP,
+  pretty_setmarginP, print_commandsP, print_theoryP, print_syntaxP,
+  print_attributesP, print_methodsP, print_theoremsP, print_bindsP,
+  print_lthmsP, print_thmsP, print_propP, print_termP, print_typeP,
   (*system commands*)
   cdP, pwdP, use_thyP, use_thy_onlyP, update_thyP, update_thy_onlyP,
   touch_thyP, touch_all_thysP, remove_thyP, prP, commitP, quitP,