--- a/src/Pure/Syntax/parser.ML Mon May 08 21:50:21 2023 +0200
+++ b/src/Pure/Syntax/parser.ML Mon May 08 23:00:17 2023 +0200
@@ -7,6 +7,7 @@
signature PARSER =
sig
+ val timing: bool Unsynchronized.ref
type gram
val empty_gram: gram
val extend_gram: Syntax_Ext.xprod list -> gram -> gram
@@ -415,6 +416,8 @@
(** operations on grammars **)
+val timing = Unsynchronized.ref true;
+
val empty_gram =
Gram
{nt_count = 0,
@@ -426,8 +429,8 @@
(*Add productions to a grammar*)
-fun extend_gram [] gram = gram
- | extend_gram xprods (Gram {nt_count, prod_count, tags, chains, lambdas, prods}) =
+fun extend_gram0 [] gram = gram
+ | extend_gram0 xprods (Gram {nt_count, prod_count, tags, chains, lambdas, prods}) =
let
(*Get tag for existing nonterminal or create a new one*)
fun get_tag nt_count tags nt =
@@ -490,6 +493,12 @@
prods = Array.vector prods'}
end;
+fun extend_gram xprods gram =
+ if ! timing then
+ Timing.cond_timeit true ("Parser.extend_gram" ^ Position.here (Position.thread_data ()))
+ (fn () => extend_gram0 xprods gram)
+ else extend_gram0 xprods gram;
+
fun make_gram xprods = extend_gram xprods empty_gram;