src/Pure/Isar/isar_syn.ML
changeset 14934 bf9f525d4821
parent 14900 c66394c408f7
child 14950 e22fad2b6f6f
equal deleted inserted replaced
14933:3fd8c03e3ee6 14934:bf9f525d4821
   700     (P.name >> (Toplevel.no_timing oo IsarCmd.remove_thy));
   700     (P.name >> (Toplevel.no_timing oo IsarCmd.remove_thy));
   701 
   701 
   702 val kill_thyP =
   702 val kill_thyP =
   703   OuterSyntax.improper_command "kill_thy" "kill theory -- try to remove from loader database"
   703   OuterSyntax.improper_command "kill_thy" "kill theory -- try to remove from loader database"
   704     K.diag (P.name >> (Toplevel.no_timing oo IsarCmd.kill_thy));
   704     K.diag (P.name >> (Toplevel.no_timing oo IsarCmd.kill_thy));
       
   705 
       
   706 val display_draftsP =
       
   707   OuterSyntax.improper_command "display_drafts" "display raw source files with symbols"
       
   708     K.diag (Scan.repeat1 P.name >> (Toplevel.no_timing oo IsarCmd.display_drafts));
       
   709 
       
   710 val print_draftsP =
       
   711   OuterSyntax.improper_command "print_drafts" "print raw source files with symbols"
       
   712     K.diag (Scan.repeat1 P.name >> (Toplevel.no_timing oo IsarCmd.print_drafts));
   705 
   713 
   706 val opt_limits =
   714 val opt_limits =
   707   Scan.option P.nat -- Scan.option (P.$$$ "," |-- P.!!! P.nat);
   715   Scan.option P.nat -- Scan.option (P.$$$ "," |-- P.!!! P.nat);
   708 
   716 
   709 val prP =
   717 val prP =
   785   print_casesP, print_introsP, print_thmsP, print_prfsP, print_full_prfsP,
   793   print_casesP, print_introsP, print_thmsP, print_prfsP, print_full_prfsP,
   786   print_propP, print_termP, print_typeP,
   794   print_propP, print_termP, print_typeP,
   787   (*system commands*)
   795   (*system commands*)
   788   cdP, pwdP, use_thyP, use_thy_onlyP, update_thyP, update_thy_onlyP,
   796   cdP, pwdP, use_thyP, use_thy_onlyP, update_thyP, update_thy_onlyP,
   789   touch_thyP, touch_all_thysP, touch_child_thysP, remove_thyP,
   797   touch_thyP, touch_all_thysP, touch_child_thysP, remove_thyP,
   790   kill_thyP, prP, disable_prP, enable_prP, commitP, quitP, exitP,
   798   kill_thyP, display_draftsP, print_draftsP, prP, disable_prP,
   791   init_toplevelP, welcomeP];
   799   enable_prP, commitP, quitP, exitP, init_toplevelP, welcomeP];
   792 
   800 
   793 end;
   801 end;
   794 
   802 
   795 
   803 
   796 (*install the Pure outer syntax*)
   804 (*install the Pure outer syntax*)