Fixing #1960 (xml bug with external on goal variable) and #1961

(anomaly while parsing $ not followed by an ident).



git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11785 85f007b7-540e-0410-9357-904b9bb8a0f7

6 files changed, 23 insertions, 37 deletions

diff --git a/contrib/xml/cic2Xml.ml b/contrib/xml/cic2Xml.ml
index f04a03f9fd..08d3a85010 100644
--- a/contrib/xml/cic2Xml.ml
+++ b/contrib/xml/cic2Xml.ml
@@ -7,7 +7,7 @@ let print_xml_term ch env sigma cic =
   let seed = ref 0 in
   let acic =
    Cic2acic.acic_of_cic_context' true seed ids_to_terms constr_to_ids 
-    ids_to_father_ids ids_to_inner_sorts ids_to_inner_types []
+    ids_to_father_ids ids_to_inner_sorts ids_to_inner_types
     env [] sigma (Unshare.unshare cic) None in
   let xml = Acic2Xml.print_term ids_to_inner_sorts acic in
   Xml.pp_ch xml ch
diff --git a/contrib/xml/cic2acic.ml b/contrib/xml/cic2acic.ml
index 1a6cb9c811..c62db00bb1 100644
--- a/contrib/xml/cic2acic.ml
+++ b/contrib/xml/cic2acic.ml
@@ -349,7 +349,7 @@ let source_id_of_id id = "#source#" ^ id;;
 
 let acic_of_cic_context' computeinnertypes seed ids_to_terms constr_to_ids
  ids_to_father_ids ids_to_inner_sorts ids_to_inner_types
- pvars ?(fake_dependent_products=false) env idrefs evar_map t expectedty
+ ?(fake_dependent_products=false) env idrefs evar_map t expectedty
 =
  let module D = DoubleTypeInference in
  let module E = Environ in
@@ -541,6 +541,8 @@ print_endline "PASSATO" ; flush stdout ;
                 add_inner_type fresh_id'' ;
                A.ARel (fresh_id'', n, List.nth idrefs (n-1), id)
            | T.Var id ->
+	      let pvars = Termops.ids_of_named_context (E.named_context env) in
+	      let pvars = List.map N.string_of_id pvars in
               let path = get_uri_of_var (N.string_of_id id) pvars in
                Hashtbl.add ids_to_inner_sorts fresh_id'' innersort ;
                if is_a_Prop innersort  && expected_available then
@@ -827,6 +829,7 @@ print_endline "PASSATO" ; flush stdout ;
      aux computeinnertypes None [] env idrefs t
 ;;
 
+(* Obsolete [HH 1/2009]
 let acic_of_cic_context metasenv context t =
  let ids_to_terms = Hashtbl.create 503 in
  let constr_to_ids = Acic.CicHash.create 503 in
@@ -838,8 +841,9 @@ let acic_of_cic_context metasenv context t =
     ids_to_inner_sorts ids_to_inner_types metasenv context t,
    ids_to_terms, ids_to_father_ids, ids_to_inner_sorts, ids_to_inner_types
 ;;
+*)
 
-let acic_object_of_cic_object pvars sigma obj =
+let acic_object_of_cic_object sigma obj =
  let module A = Acic in
   let ids_to_terms = Hashtbl.create 503 in
   let constr_to_ids = Acic.CicHash.create 503 in
@@ -853,7 +857,7 @@ let acic_object_of_cic_object pvars sigma obj =
   let seed = ref 0 in
   let acic_term_of_cic_term_context' =
    acic_of_cic_context' true seed ids_to_terms constr_to_ids ids_to_father_ids
-    ids_to_inner_sorts ids_to_inner_types pvars in
+    ids_to_inner_sorts ids_to_inner_types in
 (*CSC: is this the right env to use? Hhmmm. There is a problem: in    *)
 (*CSC: Global.env () the object we are exporting is already defined,  *)
 (*CSC: either in the environment or in the named context (in the case *)
diff --git a/contrib/xml/proofTree2Xml.ml4 b/contrib/xml/proofTree2Xml.ml4
index 26b1b0b760..a501fb6a63 100644
--- a/contrib/xml/proofTree2Xml.ml4
+++ b/contrib/xml/proofTree2Xml.ml4
@@ -31,7 +31,6 @@ let constr_to_xml obj sigma env =
   let ids_to_inner_sorts = Hashtbl.create 503 in
   let ids_to_inner_types = Hashtbl.create 503 in
 
-  let pvars = [] in
   (* named_context holds section variables and local variables *)
   let named_context = Environ.named_context env  in
   (* real_named_context holds only the section variables *)
@@ -54,7 +53,7 @@ let constr_to_xml obj sigma env =
    try
     let annobj =
      Cic2acic.acic_of_cic_context' false seed ids_to_terms constr_to_ids
-      ids_to_father_ids ids_to_inner_sorts ids_to_inner_types pvars rel_env
+      ids_to_father_ids ids_to_inner_sorts ids_to_inner_types rel_env
       idrefs sigma (Unshare.unshare obj') None
     in
      Acic2Xml.print_term ids_to_inner_sorts annobj
diff --git a/contrib/xml/xmlcommand.ml b/contrib/xml/xmlcommand.ml
index 4ee97813bd..1ae1866144 100644
--- a/contrib/xml/xmlcommand.ml
+++ b/contrib/xml/xmlcommand.ml
@@ -79,15 +79,6 @@ let could_have_namesakes o sp =      (* namesake = omonimo in italian *)
     | _                 -> false  (* uninteresting thing that won't be printed*)
 ;;
 
-
-(* A SIMPLE DATA STRUCTURE AND SOME FUNCTIONS TO MANAGE THE CURRENT *)
-(* ENVIRONMENT (= [(name1,l1); ...;(namen,ln)] WHERE li IS THE LIST *)
-(* OF VARIABLES DECLARED IN THE i-th SUPER-SECTION OF THE CURRENT   *)
-(* SECTION, WHOSE PATH IS namei                                     *)
-
-let pvars = ref ([] : string list);;
-let cumenv = ref Environ.empty_env;;
-
 (* filter_params pvars hyps *)
 (* filters out from pvars (which is a list of lists) all the variables *)
 (* that does not belong to hyps (which is a simple list)               *)
@@ -120,22 +111,6 @@ type variables_type =
  | Assumption of string * Term.constr
 ;;
 
-let add_to_pvars x =
- let module E = Environ in
-  let v =
-   match x with
-      Definition (v, bod, typ) ->
-       cumenv :=
-         E.push_named (Names.id_of_string v, Some bod, typ) !cumenv ;
-       v
-    | Assumption (v, typ) ->
-       cumenv :=
-         E.push_named (Names.id_of_string v, None, typ) !cumenv ;
-       v
-  in
-  pvars := v::!pvars
-;;
-
 (* The computation is very inefficient, but we can't do anything *)
 (* better unless this function is reimplemented in the Declare   *)
 (* module.                                                       *)
@@ -231,7 +206,7 @@ let print_object uri obj sigma proof_tree_infos filename =
        ignore (Unix.system ("gzip " ^ fn' ^ ".xml"))
  in
   let (annobj,_,constr_to_ids,_,ids_to_inner_sorts,ids_to_inner_types,_,_) =
-   Cic2acic.acic_object_of_cic_object !pvars sigma obj in
+   Cic2acic.acic_object_of_cic_object sigma obj in
   let (xml, xml') = Acic2Xml.print_object uri ids_to_inner_sorts annobj in
   let xmltypes =
    Acic2Xml.print_inner_types uri ids_to_inner_sorts ids_to_inner_types in
diff --git a/parsing/lexer.ml4 b/parsing/lexer.ml4
index 5984f7415d..045c2ecca8 100644
--- a/parsing/lexer.ml4
+++ b/parsing/lexer.ml4
@@ -372,6 +372,16 @@ let process_chars bp c cs =
     | Some t -> (("", t), (bp, ep))
     | None -> err (bp, ep) Undefined_token
 
+let parse_after_dollar bp =
+  parser
+  | [< ' ('a'..'z' | 'A'..'Z' | '_' as c); len = ident_tail (store 0 c) >] -> 
+      ("METAIDENT", get_buff len)
+  | [< s >] ->
+      match lookup_utf8 s with
+      | Utf8Token (UnicodeLetter, n) ->
+	  ("METAIDENT", get_buff (ident_tail (nstore n 0 s) s))
+      | AsciiChar | Utf8Token _ | EmptyStream -> fst (process_chars bp '$' s)
+
 (* Parse what follows a dot *)
 let parse_after_dot bp c =
   parser
@@ -399,10 +409,8 @@ let parse_after_qmark bp s =
 let rec next_token = parser bp
   | [< '' ' | '\t' | '\n' |'\r' as c; s >] ->
       comm_loc bp; push_char c; next_token s
-  | [< ''$'; ' ('a'..'z' | 'A'..'Z' | '_' as c); 
-      len = ident_tail (store 0 c) >] ep -> 
-      comment_stop bp;
-      (("METAIDENT", get_buff len), (bp,ep))
+  | [< ''$'; t = parse_after_dollar bp >] ep ->
+      comment_stop bp; (t, (ep, bp))
   | [< ''.' as c; t = parse_after_dot bp c >] ep ->
       comment_stop bp;
       if Flags.do_beautify() & t=("",".") then between_com := true;
diff --git a/toplevel/metasyntax.ml b/toplevel/metasyntax.ml
index 4b4abe63ad..234dd04c42 100644
--- a/toplevel/metasyntax.ml
+++ b/toplevel/metasyntax.ml
@@ -410,7 +410,7 @@ let is_operator s =
   let l = String.length s in l <> 0 &
   (s.[0] = '+' or s.[0] = '*' or s.[0] = '=' or
    s.[0] = '-' or s.[0] = '/' or s.[0] = '<' or s.[0] = '>' or
-   s.[0] = '@' or s.[0] = '\\' or s.[0] = '&' or s.[0] = '~')
+   s.[0] = '@' or s.[0] = '\\' or s.[0] = '&' or s.[0] = '~' or s.[0] = '$')
 
 let is_prod_ident = function
   | Terminal s when is_letter s.[0] or s.[0] = '_' -> true