diff options
| author | Maxime Dénès | 2018-11-29 15:37:26 +0100 |
|---|---|---|
| committer | Maxime Dénès | 2018-12-13 10:08:02 +0100 |
| commit | e20a12d92c7cc7c40ee0ac0b6569b0ee5e0e0b0f (patch) | |
| tree | 1c9d80fb70c9df0a28e7fc8989e931cffb787b08 /interp | |
| parent | d9a6d4814f0669b586ca5c13d6d6540cd194b45f (diff) | |
Move shallow state logic to the function preparing state for workers
Diffstat (limited to 'interp')
| -rw-r--r-- | interp/notation.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/interp/notation.ml b/interp/notation.ml index c866929234..b0854de4a3 100644 --- a/interp/notation.ml +++ b/interp/notation.ml @@ -1902,7 +1902,7 @@ let pr_visibility prglob = function (**********************************************************************) (* Synchronisation with reset *) -let freeze _ = +let freeze ~marshallable = (!scope_map, !scope_stack, !uninterp_scope_stack, !arguments_scope, !delimiters_map, !notations_key_table, !scope_class_map, !prim_token_interp_infos, !prim_token_uninterp_infos, @@ -1939,7 +1939,7 @@ let _ = Summary.init_function = init } let with_notation_protection f x = - let fs = freeze false in + let fs = freeze ~marshallable:false in try let a = f x in unfreeze fs; a with reraise -> let reraise = CErrors.push reraise in |