From 2d3d1750a0012ebc45f97d0000c01141623fc634 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Tue, 28 Jul 2009 15:45:42 +0000 Subject: [PATCH] "..." -> "\ldots" for implicit vectors --- helm/software/components/acic_content/cicNotationPp.ml | 2 +- helm/software/components/content_pres/cicNotationLexer.ml | 2 -- helm/software/components/content_pres/cicNotationParser.ml | 2 +- helm/software/components/content_pres/termContentPres.ml | 2 +- helm/software/components/ng_kernel/nCicPp.ml | 2 +- 5 files changed, 4 insertions(+), 6 deletions(-) diff --git a/helm/software/components/acic_content/cicNotationPp.ml b/helm/software/components/acic_content/cicNotationPp.ml index 1e759930a..c82919f4d 100644 --- a/helm/software/components/acic_content/cicNotationPp.ml +++ b/helm/software/components/acic_content/cicNotationPp.ml @@ -144,7 +144,7 @@ let rec pp_term ?(pp_parens = true) t = | Ast.Uri (name, Some substs) -> sprintf "%s \\subst [%s]" name (pp_substs substs) | Ast.Implicit `Vector -> "?" - | Ast.Implicit `JustOne -> "..." + | Ast.Implicit `JustOne -> "…" | Ast.Meta (index, substs) -> sprintf "%d[%s]" index (String.concat "; " diff --git a/helm/software/components/content_pres/cicNotationLexer.ml b/helm/software/components/content_pres/cicNotationLexer.ml index 1dab53582..21031d002 100644 --- a/helm/software/components/content_pres/cicNotationLexer.ml +++ b/helm/software/components/content_pres/cicNotationLexer.ml @@ -69,7 +69,6 @@ let regexp delim_end = "\\]" let regexp qkeyword = "'" ( ident | pident ) "'" let regexp implicit = '?' -let regexp implicit_vector = "..." let regexp placeholder = '%' let regexp meta = implicit number @@ -317,7 +316,6 @@ and level2_ast_token = let s = Ulexing.utf8_lexeme lexbuf in return lexbuf ("META", String.sub s 1 (String.length s - 1)) | implicit -> return lexbuf ("IMPLICIT", "") - | implicit_vector -> return lexbuf ("IMPLICITVECTOR", "") | placeholder -> return lexbuf ("PLACEHOLDER", "") | ident -> handle_keywords lexbuf (Hashtbl.mem !level2_ast_keywords) "IDENT" | variable_ident -> return lexbuf ("IDENT", Ulexing.utf8_lexeme lexbuf) diff --git a/helm/software/components/content_pres/cicNotationParser.ml b/helm/software/components/content_pres/cicNotationParser.ml index 2ac6b7e6a..af9edd9be 100644 --- a/helm/software/components/content_pres/cicNotationParser.ml +++ b/helm/software/components/content_pres/cicNotationParser.ml @@ -757,7 +757,7 @@ EXTEND | r = NREF -> return_term loc (Ast.NRef (NReference.reference_of_string r)) | n = NUMBER -> return_term loc (Ast.Num (n, 0)) | IMPLICIT -> return_term loc (Ast.Implicit `JustOne) - | IMPLICITVECTOR -> return_term loc (Ast.Implicit `Vector) + | SYMBOL <:unicode> -> return_term loc (Ast.Implicit `Vector) | PLACEHOLDER -> return_term loc Ast.UserInput | m = META -> return_term loc (Ast.Meta (int_of_string m, [])) | m = META; s = meta_substs -> diff --git a/helm/software/components/content_pres/termContentPres.ml b/helm/software/components/content_pres/termContentPres.ml index 5e8f26a4f..c115fe018 100644 --- a/helm/software/components/content_pres/termContentPres.ml +++ b/helm/software/components/content_pres/termContentPres.ml @@ -254,7 +254,7 @@ let pp_ast0 t k = (fst_row :: List.flatten tl_rows @ [ break; keyword "in"; break; k where ]))) | Ast.Implicit `JustOne -> builtin_symbol "?" - | Ast.Implicit `Vector -> builtin_symbol "..." + | Ast.Implicit `Vector -> builtin_symbol "…" | Ast.Meta (n, l) -> let local_context l = List.map (function None -> None | Some t -> Some (k t)) l diff --git a/helm/software/components/ng_kernel/nCicPp.ml b/helm/software/components/ng_kernel/nCicPp.ml index a7b6559a6..7d7a90dcc 100644 --- a/helm/software/components/ng_kernel/nCicPp.ml +++ b/helm/software/components/ng_kernel/nCicPp.ml @@ -60,7 +60,7 @@ let string_of_implicit_annotation = function | `Hole -> "□" | `Term -> "Term" | `Typeof x -> "Ty("^string_of_int x^")" - | `Vector -> "..." + | `Vector -> "…" ;; let ppterm ~formatter:f ~context ~subst ~metasenv:_ ?(inside_fix=false) t = -- 2.39.2