--- 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 *)
--- 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,