From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Tue, 18 Mar 2003 13:01:31 +0000 (+0000)
Subject: Partial upgrade to the new disambiguating lexer/parser.
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=e560785956aebcb85b85f48150b3f295b825dd2a;p=helm.git

Partial upgrade to the new disambiguating lexer/parser.
---

diff --git a/helm/searchEngine/searchEngine.ml b/helm/searchEngine/searchEngine.ml
index 15fb92de7..7fa835d8c 100644
--- a/helm/searchEngine/searchEngine.ml
+++ b/helm/searchEngine/searchEngine.ml
@@ -149,13 +149,15 @@ let callback (req: Http_types.request) outchan =
         let rec parse_tokens keys lookup = function (* TODO spostarla fuori *)
           | [] -> keys, lookup
           | "alias" :: key :: value :: rest ->
-              parse_tokens
-                (key::keys)
-                (fun id ->
-                  if id = key then
-                    Some (MQueryMisc.cic_textual_parser_uri_of_string value)
-                  else lookup id)
-                rest
+              let key' = CicTextualParser0.Id key in
+               parse_tokens
+                 (key'::keys)
+                 (fun id ->
+                   if id = key' then
+                     Some
+                      (CicTextualParser0.Uri (MQueryMisc.cic_textual_parser_uri_of_string value))
+                   else lookup id)
+                 rest
           | _ -> failwith "Can't parse aliases"
         in
         let parse_choices choices_raw =
@@ -174,7 +176,8 @@ let callback (req: Http_types.request) outchan =
             (fun _ -> None)
             choices
         in
-        let id_to_uris = parse_tokens [] (fun _ -> None) tokens in
+        let (id_to_uris : Disambiguate.domain_and_interpretation) =
+         parse_tokens [] (fun _ -> None) tokens in
         let id_to_choices =
           try
             let choices_raw = req#param "choices" in
@@ -184,6 +187,12 @@ let callback (req: Http_types.request) outchan =
         let module Chat: Disambiguate.Callbacks =
           struct
 
+            let get_metasenv () =
+             !CicTextualParser0.metasenv
+
+            let set_metasenv metasenv =
+              CicTextualParser0.metasenv := metasenv
+
             let output_html = prerr_endline
 
             let interactive_user_uri_choice
@@ -283,12 +292,15 @@ let callback (req: Http_types.request) outchan =
                         (List.map
                           (fun name ->
                             sprintf "\"alias %s cic:%s\""
-                              name
+                              (match name with
+                                  CicTextualParser0.Id name -> name
+                                | _ -> assert false (*CSC: completare *))
                               (match f name with
                               | None -> assert false
-                              | Some t ->
+                              | Some (CicTextualParser0.Uri t) ->
                                   MQueryMisc.string_of_cic_textual_parser_uri
-                                    t))
+                                    t
+                              | _ -> assert false (*CSC: completare *)))
                           domain)
                 in
                 let processed_line =