diff options
author | 2010-03-29 21:48:43 +0000 | |
---|---|---|
committer | 2010-03-29 21:48:43 +0000 | |
commit | a4a492ca1c1fe2caa3f5de785fe08662d9520725 (patch) | |
tree | f38723f9251f49f5352d3b18ce10ea9263c1cdf6 /interp/notation.ml | |
parent | 8bc1219464471054cd5f683c33bfa7ddf76802f6 (diff) |
Several bug-fixes and improvements of coqdoc
- make links to section variables working (used qualified names for
disambiguation and fixed the place in intern_var where to dump them)
(wish #2277)
- mapping of physical to logical paths now follows coq (see bug #2274)
(incidentally, it was also incorrectly seeing foobar.v as a in directory foo)
- added links for notations
- added new category "other" for indexing entries not starting with latin letter
(e.g. notations or non-latin identifiers which was otherwise broken)
- protected non-notation strings (from String.v) from utf8 symbol interpretation
- incidentally quoted parseable _ in notations to avoid confusion with
placeholder in the "_ + _" form of notation
- improved several "Sys_error" error messages
- fixed old bug about second dot of ".." being interpreted as regular dot
- removed obsolete lexer in index.mll (and renamed index.mll to index.ml)
- added a test-suite file for testing various features of coqdoc
Things that still do not work:
- when a notation is redefined several times in the same scope, only
the link to the first definition works
- if chars and symbols are not separated in advance, idents
that immediately follow symbols are not detected
(e.g. as in {True}+{True} where coqdoc sees a symbol "+{True}")
- parentheses, curly brackets and semi-colon not linked in notations
Things that can probably be improved:
- all notations are indexed in the same category "other"; can we do better?
- all non-latin identifiers (e.g. Greek letters) are also indexed in the
same "other" category; can we do better?
- globalization data for notations could be compacted (currently there is one
line per each proper location covered by the notation)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12890 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'interp/notation.ml')
-rw-r--r-- | interp/notation.ml | 5 |
1 files changed, 3 insertions, 2 deletions
diff --git a/interp/notation.ml b/interp/notation.ml index 39ae27823..bee6c5c93 100644 --- a/interp/notation.ml +++ b/interp/notation.ml @@ -42,7 +42,7 @@ open Ppextend type level = precedence * tolerability list type delimiters = string -type notation_location = dir_path * string +type notation_location = (dir_path * dir_path) * string type scope = { notations: (string, interpretation * notation_location) Gmap.t; @@ -355,7 +355,7 @@ let find_prim_token g loc p sc = (* Try for a primitive numerical notation *) let (spdir,interp) = Hashtbl.find prim_token_interpreter_tab sc loc p in check_required_module loc sc spdir; - g (interp ()), (dirpath (fst spdir),"") + g (interp ()), ((dirpath (fst spdir),empty_dirpath),"") let interp_prim_token_gen g loc p local_scopes = let scopes = make_current_scopes local_scopes in @@ -536,6 +536,7 @@ type symbol = let rec string_of_symbol = function | NonTerminal _ -> ["_"] + | Terminal "_" -> ["'_'"] | Terminal s -> [s] | SProdList (_,l) -> let l = List.flatten (List.map string_of_symbol l) in "_"::l@".."::l@["_"] |