1 package acl2s.plugin.editors.session;
2
3 import org.eclipse.jface.text.IDocument;
4 import org.eclipse.jface.text.IRegion;
5 import org.eclipse.jface.text.ITextViewer;
6 import org.eclipse.jface.text.Region;
7 import org.eclipse.jface.text.hyperlink.IHyperlink;
8 import org.eclipse.jface.text.hyperlink.IHyperlinkDetector;
9 import org.eclipse.jface.text.hyperlink.URLHyperlink;
10
11 import acl2s.lib.session.IBaseConfig;
12
13 public class Acl2DocHyperlinkDetector implements IHyperlinkDetector {
14 IBaseConfig config;
15
16 static final String specialDocSectionChars = "!-$*/+=<>@";
17
18 public Acl2DocHyperlinkDetector(IBaseConfig config) {
19 this.config = config;
20 }
21
22 static boolean docSectionChar(char c) {
23 return Character.isLetterOrDigit(c) || specialDocSectionChars.indexOf(c) >= 0;
24 }
25
26 static String acl2HtmlEscape(String name) {
27 StringBuilder ret = new StringBuilder();
28 for (int i = 0; i < name.length(); i++) {
29 switch (name.charAt(i)) {
30 case '/': ret.append("_slash_"); break;
31 case '\\': ret.append("_backslash_"); break;
32 case '&': ret.append("_ampersand_"); break;
33 case ' ': ret.append("_"); break;
34 case ':': ret.append("_colon_"); break;
35 case '<': ret.append("_lt_"); break;
36 case '>': ret.append("_gt_"); break;
37 case '*': ret.append("_star_"); break;
38 case '?': ret.append("_qm_"); break;
39 case '@': ret.append("_at_"); break;
40 case '!': ret.append("_bang_"); break;
41 case '(': ret.append("_lparen_"); break;
42 case ')': ret.append("_rparen_"); break;
43 case '_': ret.append("_underscore_"); break;
44 default: ret.append(name.charAt(i));
45 }
46 }
47 return ret.toString();
48 }
49
50 public IHyperlink[] detectHyperlinks(ITextViewer textViewer,
51 IRegion r, boolean canShowMultipleHyperlinks) {
52 if (r == null || textViewer == null)
53 return null;
54 IDocument doc = textViewer.getDocument();
55 IHyperlink ret = null;
56
57 //String text = MyTypedRegion.getStringFromDocumentRegion(doc,r);
58 String text = doc.get();
59 int pos = r.getOffset()-1;
60 int end = r.getOffset() + r.getLength();
61
62 pos = text.lastIndexOf(":DOC", end);
63
64 if (pos < 0 || pos >= end || pos < r.getOffset()-100) return null;
65
66 int thisStart = pos;
67 pos += 4;
68 if (pos < text.length() && Character.isWhitespace(text.charAt(pos))) {
69 do { pos++;
70 } while (pos < text.length() && Character.isWhitespace(text.charAt(pos)));
71 if (pos < text.length() && docSectionChar(text.charAt(pos))) {
72 int nameStart = pos;
73 do { pos++;
74 } while (pos < text.length() && docSectionChar(text.charAt(pos)));
75 if (pos + 3 < text.length() && "(R)".equals(text.substring(pos,pos+3))) {
76 pos += 3;
77 }
78 if (pos >= r.getOffset()) {
79 String name = text.substring(nameStart,pos);
80 if (name.toLowerCase().equals(name)) {
|
Event do_not_call: |
"java.lang.String.toUpperCase()" implicitly uses the environment's default character set, which might lead to unexpected behavior. Consider using toUpperCase(Locale locale). |
81 name = name.toUpperCase();
82 }
83 name = acl2HtmlEscape(name);
84 Region urlr = new Region(thisStart,pos-thisStart);
85 String urlstr = config.getDocBaseURL() + name + ".html";
86 ret = new URLHyperlink(urlr,urlstr);
87 }
88 }
89 }
90
91 return ret == null ? null : new IHyperlink[] { ret };
92 }
93 }