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 /parsing/esyntax.ml | |
| 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
Diffstat (limited to 'parsing/esyntax.ml')
| -rw-r--r-- | parsing/esyntax.ml | 8 |
1 files changed, 4 insertions, 4 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) |