# HG changeset patch
# User wenzelm
# Date 1683579617 -7200
# Node ID 4660181c83c984f78fb95e5cb00ed00cb04d3d3a
# Parent  afa6117bace4e438c272d59f50e10dd089f38fcd
optional timing;

diff -r afa6117bace4 -r 4660181c83c9 src/Pure/Syntax/parser.ML
--- 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;