Eureka!

[helm.git] / helm / gTopLevel / disambiguatingParser.ml

diff --git a/helm/gTopLevel/disambiguatingParser.ml b/helm/gTopLevel/disambiguatingParser.ml
index 580e09bb251bb71039b165c937d3c6dfaf975121..eb89b11700c375a204fe036194d08d173364a16c 100644 (file)
--- a/helm/gTopLevel/disambiguatingParser.ml
+++ b/helm/gTopLevel/disambiguatingParser.ml
@@ -25,14 +25,81 @@
 
 exception NoWellTypedInterpretation
 
-module EnvironmentP3 = DisambiguateTypes.EnvironmentP3
+module AndreaAndZackDisambiguatingParser =
+ struct
+  module EnvironmentP3 = DisambiguateTypes.EnvironmentP3
+
+  module Make (C : DisambiguateTypes.Callbacks) =
+   struct
+    let
+     disambiguate_term mqi_handle context metasenv term_as_string environment
+    =
+     let module Disambiguate' = Disambiguate.Make (C) in
+      let term =
+       CicTextualParser2.parse_term (Stream.of_string term_as_string)
+      in
+       Disambiguate'.disambiguate_term
+        mqi_handle context metasenv term environment
+   end
+ end
+
+
+module CSCTextualDisambiguatingParser =
+ struct
+  module EnvironmentP3 = OldDisambiguate.EnvironmentP3
+
+  module Make (C : DisambiguateTypes.Callbacks) =
+   struct
+    let
+     disambiguate_term mqi_handle context metasenv term_as_string environment
+    =
+     let module Disambiguate' = OldDisambiguate.Make (C) in
+      let name_context =
+       List.map
+        (function
+            Some (n,_) -> Some n
+          | None -> None
+        ) context
+      in
+       let lexbuf = Lexing.from_string term_as_string in
+        let dom,mk_metasenv_and_expr =
+         CicTextualParserContext.main
+          ~context:name_context ~metasenv CicTextualLexer.token lexbuf
+        in
+         Disambiguate'.disambiguate_input mqi_handle
+          context metasenv dom mk_metasenv_and_expr environment
+   end
+ end
 
-module Make (C : DisambiguateTypes.Callbacks) =
+module CSCTexDisambiguatingParser =
  struct
-  let disambiguate_term mqi_handle context metasenv term_as_string environment =
-   let module Disambiguate' = Disambiguate.Make (C) in
-    let term = CicTextualParser2.parse_term (Stream.of_string term_as_string) in
-     Disambiguate'.disambiguate_term
-      mqi_handle context metasenv term environment
+  module EnvironmentP3 = OldDisambiguate.EnvironmentP3
+
+  module Make (C : DisambiguateTypes.Callbacks) =
+   struct
+    let
+     disambiguate_term mqi_handle context metasenv term_as_string environment
+    =
+     let module Disambiguate' = OldDisambiguate.Make (C) in
+      let name_context =
+       List.map
+        (function
+            Some (n,_) -> Some n
+          | None -> None
+        ) context
+      in
+       let lexbuf = Lexing.from_string term_as_string in
+        let dom,mk_metasenv_and_expr =
+         TexCicTextualParserContext.main
+          ~context:name_context ~metasenv TexCicTextualLexer.token lexbuf
+        in
+         Disambiguate'.disambiguate_input mqi_handle
+          context metasenv dom mk_metasenv_and_expr environment
+   end
  end
-;;
+
+include AndreaAndZackDisambiguatingParser
+(*
+include CSCTextualDisambiguatingParser
+include CSCTexDisambiguatingParser
+*)