--- a/src/Pure/Isar/isar_cmd.ML Thu Oct 21 18:47:33 1999 +0200
+++ b/src/Pure/Isar/isar_cmd.ML Thu Oct 21 18:59:01 1999 +0200
@@ -11,6 +11,7 @@
val init_toplevel: Toplevel.transition -> Toplevel.transition
val exit: Toplevel.transition -> Toplevel.transition
val quit: Toplevel.transition -> Toplevel.transition
+ val touch_child_thys: string -> Toplevel.transition -> Toplevel.transition
val touch_all_thys: Toplevel.transition -> Toplevel.transition
val touch_thy: string -> Toplevel.transition -> Toplevel.transition
val remove_thy: string -> Toplevel.transition -> Toplevel.transition
@@ -66,6 +67,7 @@
(* touch theories *)
+fun touch_child_thys name = Toplevel.imperative (fn () => ThyInfo.touch_child_thys name);
val touch_all_thys = Toplevel.imperative ThyInfo.touch_all_thys;
fun touch_thy name = Toplevel.imperative (fn () => ThyInfo.touch_thy name);
fun remove_thy name = Toplevel.imperative (fn () => ThyInfo.remove_thy name);
--- a/src/Pure/Isar/isar_syn.ML Thu Oct 21 18:47:33 1999 +0200
+++ b/src/Pure/Isar/isar_syn.ML Thu Oct 21 18:59:01 1999 +0200
@@ -554,6 +554,10 @@
OuterSyntax.improper_command "touch_all_thys" "outdate all non-finished theories" K.diag
(Scan.succeed IsarCmd.touch_all_thys);
+val touch_child_thysP =
+ OuterSyntax.improper_command "touch_child_thys" "outdate child theories" K.diag
+ (P.name >> IsarCmd.touch_child_thys);
+
val remove_thyP =
OuterSyntax.improper_command "remove_thy" "remove theory from loader database" K.diag
(P.name >> IsarCmd.remove_thy);
@@ -632,8 +636,9 @@
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, disable_prP,
- enable_prP, commitP, quitP, exitP, init_toplevelP, welcomeP];
+ touch_thyP, touch_all_thysP, touch_child_thysP, remove_thyP, prP,
+ disable_prP, enable_prP, commitP, quitP, exitP, init_toplevelP,
+ welcomeP];
end;