src/Pure/Isar/isar_syn.ML
changeset 7124 78c01842d3b5
parent 7102 ead5c234b28c
child 7140 2c02c8e212fa
     1.1 --- a/src/Pure/Isar/isar_syn.ML	Wed Jul 28 13:55:34 1999 +0200
     1.2 +++ b/src/Pure/Isar/isar_syn.ML	Wed Jul 28 18:55:35 1999 +0200
     1.3 @@ -426,6 +426,10 @@
     1.4  
     1.5  (** diagnostic commands (for interactive mode only) **)
     1.6  
     1.7 +val pretty_setmarginP =
     1.8 +  OuterSyntax.improper_command "pretty_setmargin" "change default margin for pretty printing"
     1.9 +    K.diag (P.nat >> IsarCmd.pretty_setmargin);
    1.10 +
    1.11  val print_commandsP =
    1.12    OuterSyntax.improper_command "help" "print outer syntax (global)" K.diag
    1.13      (Scan.succeed (Toplevel.imperative OuterSyntax.print_outer_syntax));
    1.14 @@ -567,9 +571,9 @@
    1.15    skip_proofP, applyP, then_applyP, proofP, alsoP, finallyP, backP,
    1.16    cannot_undoP, clear_undoP, redoP, undos_proofP, kill_proofP, undoP,
    1.17    (*diagnostic commands*)
    1.18 -  print_commandsP, print_theoryP, print_syntaxP, print_attributesP,
    1.19 -  print_methodsP, print_theoremsP, print_bindsP, print_lthmsP,
    1.20 -  print_thmsP, print_propP, print_termP, print_typeP,
    1.21 +  pretty_setmarginP, print_commandsP, print_theoryP, print_syntaxP,
    1.22 +  print_attributesP, print_methodsP, print_theoremsP, print_bindsP,
    1.23 +  print_lthmsP, print_thmsP, print_propP, print_termP, print_typeP,
    1.24    (*system commands*)
    1.25    cdP, pwdP, use_thyP, use_thy_onlyP, update_thyP, update_thy_onlyP,
    1.26    touch_thyP, touch_all_thysP, remove_thyP, prP, commitP, quitP,