summaryrefslogtreecommitdiff
path: root/toplevel/metasyntax.ml
diff options
context:
space:
mode:
authorGravatar Stephane Glondu <steph@glondu.net>2012-06-04 12:23:14 +0200
committerGravatar Stephane Glondu <steph@glondu.net>2012-06-04 12:23:14 +0200
commit86535d84cc3cffeee1dcd8545343f234e7285530 (patch)
tree9b221c283c2971f7ac151397231059e1d239e723 /toplevel/metasyntax.ml
parent39efc41237ec906226a3a53d7396d51173495204 (diff)
parent61dc740ed1c3780cccaec00d059a28f0d31d0052 (diff)
Diffstat (limited to 'toplevel/metasyntax.ml')
-rw-r--r--toplevel/metasyntax.ml12
1 files changed, 12 insertions, 0 deletions
diff --git a/toplevel/metasyntax.ml b/toplevel/metasyntax.ml
index 6a4d7251..cdeff601 100644
--- a/toplevel/metasyntax.ml
+++ b/toplevel/metasyntax.ml
@@ -986,6 +986,18 @@ let inNotation : notation_obj -> obj =
classify_function = classify_notation}
(**********************************************************************)
+
+let with_lib_stk_protection f x =
+ let fs = Lib.freeze () in
+ try let a = f x in Lib.unfreeze fs; a
+ with e -> Lib.unfreeze fs; raise e
+
+let with_syntax_protection f x =
+ with_lib_stk_protection
+ (with_grammar_rule_protection
+ (with_notation_protection f)) x
+
+(**********************************************************************)
(* Recovering existing syntax *)
let contract_notation ntn =