src/Pure/Isar/isar_syn.ML
changeset 7931 fa6fec415492
parent 7908 0b191b36ad97
child 8097 80a3c30d088b
equal deleted inserted replaced
7930:220892918bd1 7931:fa6fec415492
   560 
   560 
   561 val remove_thyP =
   561 val remove_thyP =
   562   OuterSyntax.improper_command "remove_thy" "remove theory from loader database" K.diag
   562   OuterSyntax.improper_command "remove_thy" "remove theory from loader database" K.diag
   563     (P.name >> IsarCmd.remove_thy);
   563     (P.name >> IsarCmd.remove_thy);
   564 
   564 
       
   565 val kill_thyP =
       
   566   OuterSyntax.improper_command "kill_thy" "kill theory -- try to remove from loader database"
       
   567     K.diag (P.name >> IsarCmd.kill_thy);
       
   568 
   565 val prP =
   569 val prP =
   566   OuterSyntax.improper_command "pr" "print current toplevel state" K.diag
   570   OuterSyntax.improper_command "pr" "print current toplevel state" K.diag
   567     (Scan.succeed (Toplevel.print o Toplevel.imperative (fn () => Toplevel.quiet := false)));
   571     (Scan.succeed (Toplevel.print o Toplevel.imperative (fn () => Toplevel.quiet := false)));
   568 
   572 
   569 val disable_prP =
   573 val disable_prP =
   572 
   576 
   573 val enable_prP =
   577 val enable_prP =
   574   OuterSyntax.improper_command "enable_pr" "enable printing of toplevel state" K.diag
   578   OuterSyntax.improper_command "enable_pr" "enable printing of toplevel state" K.diag
   575     (Scan.succeed (Toplevel.imperative (fn () => Toplevel.quiet := false)));
   579     (Scan.succeed (Toplevel.imperative (fn () => Toplevel.quiet := false)));
   576 
   580 
   577 
       
   578 val opt_unit = Scan.optional (P.$$$ "(" -- P.$$$ ")" >> (K ())) ();
       
   579 
       
   580 val commitP =
   581 val commitP =
   581   OuterSyntax.improper_command "commit" "commit current session to ML database" K.diag
   582   OuterSyntax.improper_command "commit" "commit current session to ML database" K.diag
   582     (opt_unit >> (K IsarCmd.use_commit));
   583     (P.opt_unit >> (K IsarCmd.use_commit));
   583 
   584 
   584 val quitP =
   585 val quitP =
   585   OuterSyntax.improper_command "quit" "quit Isabelle" K.control
   586   OuterSyntax.improper_command "quit" "quit Isabelle" K.control
   586     (opt_unit >> (K IsarCmd.quit));
   587     (P.opt_unit >> (K IsarCmd.quit));
   587 
   588 
   588 val exitP =
   589 val exitP =
   589   OuterSyntax.improper_command "exit" "exit Isar loop" K.control
   590   OuterSyntax.improper_command "exit" "exit Isar loop" K.control
   590     (Scan.succeed IsarCmd.exit);
   591     (Scan.succeed IsarCmd.exit);
   591 
   592 
   634   print_syntaxP, print_theoremsP, print_attributesP, print_methodsP,
   635   print_syntaxP, print_theoremsP, print_attributesP, print_methodsP,
   635   thms_containingP, print_bindsP, print_lthmsP, print_thmsP,
   636   thms_containingP, print_bindsP, print_lthmsP, print_thmsP,
   636   print_propP, print_termP, print_typeP,
   637   print_propP, print_termP, print_typeP,
   637   (*system commands*)
   638   (*system commands*)
   638   cdP, pwdP, use_thyP, use_thy_onlyP, update_thyP, update_thy_onlyP,
   639   cdP, pwdP, use_thyP, use_thy_onlyP, update_thyP, update_thy_onlyP,
   639   touch_thyP, touch_all_thysP, touch_child_thysP, remove_thyP, prP,
   640   touch_thyP, touch_all_thysP, touch_child_thysP, remove_thyP,
   640   disable_prP, enable_prP, commitP, quitP, exitP, init_toplevelP,
   641   kill_thyP, prP, disable_prP, enable_prP, commitP, quitP, exitP,
   641   welcomeP];
   642   init_toplevelP, welcomeP];
   642 
   643 
   643 
   644 
   644 end;
   645 end;
   645 
   646 
   646 
   647