diff options
| author | herbelin | 2002-12-03 15:07:19 +0000 |
|---|---|---|
| committer | herbelin | 2002-12-03 15:07:19 +0000 |
| commit | baed251f7e00024b900c1ddc984cc0fce4df5cb6 (patch) | |
| tree | e953a6d767aa94c4452fed6aee48ec7a060cf205 | |
| parent | 7a1636ec58c426059ff6864edd12868087b7f93c (diff) | |
bugs d'affichage (confusion key/scope dans les délimiteurs)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3366 85f007b7-540e-0410-9357-904b9bb8a0f7
| -rw-r--r-- | parsing/esyntax.ml | 8 | ||||
| -rw-r--r-- | parsing/ppconstr.ml | 5 |
2 files changed, 6 insertions, 7 deletions
diff --git a/parsing/esyntax.ml b/parsing/esyntax.ml index 1fa8523628..c506c1ff25 100644 --- a/parsing/esyntax.ml +++ b/parsing/esyntax.ml @@ -193,7 +193,7 @@ let print_delimiters inh se strm = function let rspace = let c = right.[0] in if is_letter c or is_digit c or c = '\'' then str " " else mt () in - str left ++ lspace ++ strm ++ rspace ++ str right + hov 0 (str left ++ lspace ++ strm ++ rspace ++ str right) (* Print the syntax entry. In the unparsing hunks, the tokens are * printed using the token_printer, unless another primitive printer @@ -229,16 +229,16 @@ let call_primitive_parser rec_pr otherwise inherited scopes (se,env) = (* Look if scope [sc] associated to this printer is OK *) (match Symbols.availability_of_numeral sc scopes with | None -> otherwise () - | Some scopt -> + | Some key -> (* We can use this printer *) let node = Ast.pat_sub dummy_loc env e in match pr node with - | Some strm -> print_delimiters inherited se strm scopt + | Some strm -> print_delimiters inherited se strm key | None -> otherwise ()) | [UNP_SYMBOLIC (sc,pat,sub)] -> (match Symbols.availability_of_notation (sc,pat) scopes with | None -> otherwise () - | Some scopt -> + | Some (scopt,key) -> print_delimiters inherited se (print_syntax_entry rec_pr (option_cons scopt scopes) env {se with syn_hunks = [sub]}) scopt) diff --git a/parsing/ppconstr.ml b/parsing/ppconstr.ml index cea099da77..a8dd7b8aa1 100644 --- a/parsing/ppconstr.ml +++ b/parsing/ppconstr.ml @@ -87,9 +87,8 @@ let prec_less child (parent,assoc) = (if assoc = E then (<=) else (<)) child parent let env_assoc_value v env = - try List.assoc v env - with Not_found -> - anomaly ("Printing metavariable "^(string_of_id v)^" is unbound") + try List.nth env (v-1) + with Not_found -> anomaly "Inconsistent environment for pretty-print rule" open Symbols |