1) Matitaweb now disambiguates scripts as it runs them

[helm.git] / matitaB / components / grafite_engine / grafiteEngine.ml

diff --git a/matitaB/components/grafite_engine/grafiteEngine.ml b/matitaB/components/grafite_engine/grafiteEngine.ml
index 26ba7ffd06e404001dec125120258de453da1ecf..a0b00150f2fc5a1563a68155f7e0f2bff45ef6f2 100644 (file)
--- a/matitaB/components/grafite_engine/grafiteEngine.ml
+++ b/matitaB/components/grafite_engine/grafiteEngine.ml
@@ -771,8 +771,11 @@ let rec eval_ncommand ~include_paths opts status (text,prefix_len,cmd) =
         if dir <> Some `RightToLeft then eval_input_notation status (l1,l2)
         else status
       in
+      let status =
        if dir <> Some `LeftToRight then eval_output_notation status (l1,l2)
        else status
+      in prerr_endline ("new grammar:\n" ^ (Print_grammar.ebnf_of_term status));
+      status
   | GrafiteAst.Alias (loc, spec) -> 
      let diff =
       (*CSC: Warning: this code should be factorized with the corresponding