# 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,