src/Pure/Isar/isar_syn.ML
changeset 7222 e4244b2e70ef
parent 7199 7fede88e5c73
child 7269 8aa45a40c87a
equal deleted inserted replaced
7221:13e43b7456a1 7222:e4244b2e70ef
   525 
   525 
   526 val prP =
   526 val prP =
   527   OuterSyntax.improper_command "pr" "print current toplevel state" K.diag
   527   OuterSyntax.improper_command "pr" "print current toplevel state" K.diag
   528     (Scan.succeed (Toplevel.print o Toplevel.imperative (fn () => Toplevel.quiet := false)));
   528     (Scan.succeed (Toplevel.print o Toplevel.imperative (fn () => Toplevel.quiet := false)));
   529 
   529 
   530 val no_prP =
   530 val disable_prP =
   531   OuterSyntax.improper_command "no_pr" "disable printing of toplevel state" K.diag
   531   OuterSyntax.improper_command "disable_pr" "disable printing of toplevel state" K.diag
   532     (Scan.succeed (Toplevel.imperative (fn () => Toplevel.quiet := true)));
   532     (Scan.succeed (Toplevel.imperative (fn () => Toplevel.quiet := true)));
       
   533 
       
   534 val enable_prP =
       
   535   OuterSyntax.improper_command "enable_pr" "enable printing of toplevel state" K.diag
       
   536     (Scan.succeed (Toplevel.imperative (fn () => Toplevel.quiet := false)));
   533 
   537 
   534 
   538 
   535 val opt_unit = Scan.optional (P.$$$ "(" -- P.$$$ ")" >> (K ())) ();
   539 val opt_unit = Scan.optional (P.$$$ "(" -- P.$$$ ")" >> (K ())) ();
   536 
   540 
   537 val commitP =
   541 val commitP =
   586   pretty_setmarginP, print_commandsP, print_theoryP, print_syntaxP,
   590   pretty_setmarginP, print_commandsP, print_theoryP, print_syntaxP,
   587   print_attributesP, print_methodsP, print_theoremsP, print_bindsP,
   591   print_attributesP, print_methodsP, print_theoremsP, print_bindsP,
   588   print_lthmsP, print_thmsP, print_propP, print_termP, print_typeP,
   592   print_lthmsP, print_thmsP, print_propP, print_termP, print_typeP,
   589   (*system commands*)
   593   (*system commands*)
   590   cdP, pwdP, use_thyP, use_thy_onlyP, update_thyP, update_thy_onlyP,
   594   cdP, pwdP, use_thyP, use_thy_onlyP, update_thyP, update_thy_onlyP,
   591   touch_thyP, touch_all_thysP, remove_thyP, prP, no_prP, commitP,
   595   touch_thyP, touch_all_thysP, remove_thyP, prP, disable_prP,
   592   quitP, exitP, init_toplevelP];
   596   enable_prP, commitP, quitP, exitP, init_toplevelP];
   593 
   597 
   594 
   598 
   595 end;
   599 end;
   596 
   600 
   597 
   601