diff options
| -rw-r--r-- | src/server/PGFService.hs | 22 |
1 files changed, 13 insertions, 9 deletions
diff --git a/src/server/PGFService.hs b/src/server/PGFService.hs index 75670adbf..d79cf644b 100644 --- a/src/server/PGFService.hs +++ b/src/server/PGFService.hs @@ -327,17 +327,21 @@ doBrowse pgf id cssClass href = identifiers = PGF.functions pgf ++ PGF.categories pgf - annotate [] = [] + annotate [] = [] annotate (c:cs) - | isSpace c = c : annotate cs - | otherwise = let (id,cs') = break isSpace (c:cs) - in (if PGF.mkCId id `elem` identifiers - then mkLink id - else if id == "fun" || id == "data" || id == "cat" || id == "def" - then "<B>"++id++"</B>" - else id) ++ - annotate cs' + | isIdentInitial c = let (id,cs') = break (not . isIdentChar) (c:cs) + in (if PGF.mkCId id `elem` identifiers + then mkLink id + else if id == "fun" || id == "data" || id == "cat" || id == "def" + then "<B>"++id++"</B>" + else id) ++ + annotate cs' + | otherwise = c : annotate cs + annotateCIds ids = unwords (map (mkLink . PGF.showCId) ids) + + isIdentInitial c = isAlpha c || c == '_' + isIdentChar c = isAlphaNum c || c == '_' || c == '\'' hrefAttr id = case href of |