Source Code Cross Referenced for Linearization.java in  » Testing » KeY » de » uka » ilkd » key » ocl » gf » Java Source Code / Java DocumentationJava Source Code and Java Documentation

Java Source Code / Java Documentation
1. 6.0 JDK Core
2. 6.0 JDK Modules
3. 6.0 JDK Modules com.sun
4. 6.0 JDK Modules com.sun.java
5. 6.0 JDK Modules sun
6. 6.0 JDK Platform
7. Ajax
8. Apache Harmony Java SE
9. Aspect oriented
10. Authentication Authorization
11. Blogger System
12. Build
13. Byte Code
14. Cache
15. Chart
16. Chat
17. Code Analyzer
18. Collaboration
19. Content Management System
20. Database Client
21. Database DBMS
22. Database JDBC Connection Pool
23. Database ORM
24. Development
25. EJB Server geronimo
26. EJB Server GlassFish
27. EJB Server JBoss 4.2.1
28. EJB Server resin 3.1.5
29. ERP CRM Financial
30. ESB
31. Forum
32. GIS
33. Graphic Library
34. Groupware
35. HTML Parser
36. IDE
37. IDE Eclipse
38. IDE Netbeans
39. Installer
40. Internationalization Localization
41. Inversion of Control
42. Issue Tracking
43. J2EE
44. JBoss
45. JMS
46. JMX
47. Library
48. Mail Clients
49. Net
50. Parser
51. PDF
52. Portal
53. Profiler
54. Project Management
55. Report
56. RSS RDF
57. Rule Engine
58. Science
59. Scripting
60. Search Engine
61. Security
62. Sevlet Container
63. Source Control
64. Swing Library
65. Template Engine
66. Test Coverage
67. Testing
68. UML
69. Web Crawler
70. Web Framework
71. Web Mail
72. Web Server
73. Web Services
74. Web Services apache cxf 2.0.1
75. Web Services AXIS2
76. Wiki Engine
77. Workflow Engines
78. XML
79. XML UI
Java
Java Tutorial
Java Open Source
Jar File Download
Java Articles
Java Products
Java by API
Photoshop Tutorials
Maya Tutorials
Flash Tutorials
3ds-Max Tutorials
Illustrator Tutorials
GIMP Tutorials
C# / C Sharp
C# / CSharp Tutorial
C# / CSharp Open Source
ASP.Net
ASP.NET Tutorial
JavaScript DHTML
JavaScript Tutorial
JavaScript Reference
HTML / CSS
HTML CSS Reference
C / ANSI-C
C Tutorial
C++
C++ Tutorial
Ruby
PHP
Python
Python Tutorial
Python Open Source
SQL Server / T-SQL
SQL Server / T-SQL Tutorial
Oracle PL / SQL
Oracle PL/SQL Tutorial
PostgreSQL
SQL / MySQL
MySQL Tutorial
VB.Net
VB.Net Tutorial
Flash / Flex / ActionScript
VBA / Excel / Access / Word
XML
XML Tutorial
Microsoft Office PowerPoint 2007 Tutorial
Microsoft Office Excel 2007 Tutorial
Microsoft Office Word 2007 Tutorial
Java Source Code / Java Documentation » Testing » KeY » de.uka.ilkd.key.ocl.gf 
Source Cross Referenced  Class Diagram Java Document (Java Doc) 


001:        //Copyright (c) Janna Khegai 2004, Hans-Joachim Daniels 2005
002:        //
003:        //This program is free software; you can redistribute it and/or modify
004:        //it under the terms of the GNU General Public License as published by
005:        //the Free Software Foundation; either version 2 of the License, or
006:        //(at your option) any later version.
007:        //
008:        //This program is distributed in the hope that it will be useful,
009:        //but WITHOUT ANY WARRANTY; without even the implied warranty of
010:        //MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
011:        //GNU General Public License for more details.
012:        //
013:        //You can either finde the file LICENSE or LICENSE.TXT in the source 
014:        //distribution or in the .jar file of this application
015:
016:        package de.uka.ilkd.key.ocl.gf;
017:
018:        import java.util.HashMap;
019:        import java.util.HashSet;
020:        import java.util.Iterator;
021:        import java.util.Vector;
022:        import java.util.logging.Level;
023:        import java.util.logging.Logger;
024:
025:        /**
026:         * Encapsulates everything that has to do with the linearization.
027:         * It is parsed here, and also the indices for click-in for pure text and HTML
028:         * are managed here. They get calculated in GfCapsule.
029:         * The result can be directly displayed, and this class has methods to translate
030:         * the indices back to the respective tree positions.
031:         * @author daniels
032:         */
033:        class Linearization {
034:            /** 
035:             * linearization marking debug messages 
036:             */
037:            protected static Logger logger = Logger
038:                    .getLogger(Linearization.class.getName());
039:
040:            /**
041:             * contains all the linearization pieces as HtmlMarkedArea
042:             * Needed to know to which node in the AST a word in the linHtmlPane 
043:             * area belongs.
044:             */
045:            private Vector htmlOutputVector = new Vector();
046:            /**
047:             * the GF-output between <linearization> </linearization>  tags is stored here.
048:             * Must be saved in case the displayed languages are changed.
049:             * Only written in readLin
050:             */
051:            private String linearization = "";
052:            /** 
053:             * stack for storing the current position:
054:             * When displaying, we start with the root of the AST.
055:             * Whenever we start to display a node, it is pushed, and when it is completely displayed, we pop it.
056:             * Only LinPositions are stored in here
057:             * local in formLin?
058:             * */
059:            private Vector currentPosition = new Vector();
060:
061:            /**
062:             * Must be the same Display as GFEditor2 uses
063:             */
064:            private Display display;
065:            /**
066:             *  to collect the linearization strings 
067:             */
068:            private HashMap linearizations = new HashMap();
069:
070:            /**
071:             * Initializes this object and binds it to the given Display
072:             * @param display The display, that the editor uses
073:             */
074:            public Linearization(Display display) {
075:                this .display = display;
076:            }
077:
078:            /**
079:             * @return Returns the linearizations.
080:             */
081:            HashMap getLinearizations() {
082:                return linearizations;
083:            }
084:
085:            /**
086:             * @param linearization The linearization to set.
087:             */
088:            void setLinearization(String linearization) {
089:                this .linearization = linearization;
090:            }
091:
092:            /**
093:             * resets the output mechanism.
094:             */
095:            void reset() {
096:                htmlOutputVector = new Vector();
097:            }
098:
099:            /**
100:             * Returns the widest position (see comments to comparePositions) 
101:             * covered in the string from begin to end in the 
102:             * linearization area.
103:             * @param begin The index in htmlOutputVector of the first MarkedArea, that is possibly the max
104:             * @param end The index in htmlOutputVector of the last MarkedArea, that is possibly the max
105:             * @return the position in GF Haskell notation (hdaniels guesses)
106:             */
107:            private String findMax(int begin, int end) {
108:                String max = (((MarkedArea) this .htmlOutputVector
109:                        .elementAt(begin)).position).position;
110:                for (int i = begin + 1; i <= end; i++)
111:                    max = LinPosition
112:                            .maxPosition(max,
113:                                    (((MarkedArea) this .htmlOutputVector
114:                                            .elementAt(i)).position).position);
115:                return max;
116:            }
117:
118:            /**
119:             * Appends the string restString to display.
120:             * It parses the subtree tags and registers them.
121:             * The focus tag is expected to be replaced by subtree.
122:             * @param restString string to append, with tags in it.
123:             * @param clickable if true, the text is appended and the subtree tags are
124:             * parsed. If false, the text is appended, but the subtree tags are ignored. 
125:             * @param doDisplay true iff the output is to be displayed. 
126:             * Implies, if false, that clickable is treated as false.
127:             * @param language the current linearization language
128:             */
129:            private String appendMarked(String restString,
130:                    final boolean clickable, boolean doDisplay, String language) {
131:                String appendedPureText = "";
132:                if (restString.length() > 0) {
133:                    /** 
134:                     * the length of what is already displayed of the linearization.
135:                     * Alternatively: What has been processed in restString since
136:                     * subtreeBegin
137:                     */
138:                    int currentLength = 0;
139:                    /** position of &lt;subtree */
140:                    int subtreeBegin;
141:                    /** position of &lt;/subtree */
142:                    int subtreeEnd;
143:
144:                    if (clickable && doDisplay) {
145:                        subtreeBegin = Utils.indexOfNotEscaped(restString,
146:                                "<subtree");
147:                        subtreeEnd = Utils.indexOfNotEscaped(restString,
148:                                "</subtree");
149:                        // cutting subtree-tags:
150:                        while ((subtreeEnd > -1) || (subtreeBegin > -1)) {
151:                            /** 
152:                             * length of the portion that is to be displayed
153:                             * in the current run of appendMarked.
154:                             * For HTML this would have to be calculated
155:                             * in another way.
156:                             */
157:                            final int newLength;
158:
159:                            if ((subtreeEnd == -1)
160:                                    || ((subtreeBegin < subtreeEnd) && (subtreeBegin > -1))) {
161:                                final int subtreeTagEnd = Utils
162:                                        .indexOfNotEscaped(restString, ">",
163:                                                subtreeBegin);
164:                                final int nextOpeningTagBegin = Utils
165:                                        .indexOfNotEscaped(restString, "<",
166:                                                subtreeTagEnd);
167:
168:                                //getting position:
169:                                final int posStringBegin = Utils
170:                                        .indexOfNotEscaped(restString, "[",
171:                                                subtreeBegin);
172:                                final int posStringEnd = Utils
173:                                        .indexOfNotEscaped(restString, "]",
174:                                                subtreeBegin);
175:                                final LinPosition position = new LinPosition(
176:                                        restString.substring(posStringBegin,
177:                                                posStringEnd + 1), restString
178:                                                .substring(subtreeBegin,
179:                                                        subtreeTagEnd).indexOf(
180:                                                        "incorrect") == -1);
181:
182:                                // is something before the tag?
183:                                // is the case in the first run
184:                                if (subtreeBegin - currentLength > 1) {
185:                                    if (logger.isLoggable(Level.FINER)) {
186:                                        logger
187:                                                .finer("SOMETHING BEFORE THE TAG");
188:                                    }
189:                                    if (this .currentPosition.size() > 0)
190:                                        newLength = register(
191:                                                currentLength,
192:                                                subtreeBegin,
193:                                                (LinPosition) this .currentPosition
194:                                                        .elementAt(this .currentPosition
195:                                                                .size() - 1),
196:                                                restString, language);
197:                                    else
198:                                        newLength = register(
199:                                                currentLength,
200:                                                subtreeBegin,
201:                                                new LinPosition(
202:                                                        "[]",
203:                                                        restString
204:                                                                .substring(
205:                                                                        subtreeBegin,
206:                                                                        subtreeTagEnd)
207:                                                                .indexOf(
208:                                                                        "incorrect") == -1),
209:                                                restString, language);
210:                                } else { // nothing before the tag:
211:                                    //the case in the beginning
212:                                    if (logger.isLoggable(Level.FINER)) {
213:                                        logger.finer("NOTHING BEFORE THE TAG");
214:                                    }
215:                                    if (nextOpeningTagBegin > 0) {
216:                                        newLength = register(subtreeTagEnd + 2,
217:                                                nextOpeningTagBegin, position,
218:                                                restString, language);
219:                                    } else {
220:                                        newLength = register(subtreeTagEnd + 2,
221:                                                restString.length(), position,
222:                                                restString, language);
223:                                    }
224:                                    restString = removeSubTreeTag(restString,
225:                                            subtreeBegin, subtreeTagEnd + 1);
226:                                }
227:                                currentLength += newLength;
228:                            } else {
229:                                // something before the </subtree> tag:
230:                                if (subtreeEnd - currentLength > 1) {
231:                                    if (logger.isLoggable(Level.FINER)) {
232:                                        logger
233:                                                .finer("SOMETHING BEFORE THE </subtree> TAG");
234:                                    }
235:                                    if (this .currentPosition.size() > 0)
236:                                        newLength = register(
237:                                                currentLength,
238:                                                subtreeEnd,
239:                                                (LinPosition) this .currentPosition
240:                                                        .elementAt(this .currentPosition
241:                                                                .size() - 1),
242:                                                restString, language);
243:                                    else
244:                                        newLength = register(
245:                                                currentLength,
246:                                                subtreeEnd,
247:                                                new LinPosition(
248:                                                        "[]",
249:                                                        restString
250:                                                                .substring(
251:                                                                        subtreeBegin,
252:                                                                        subtreeEnd)
253:                                                                .indexOf(
254:                                                                        "incorrect") == -1),
255:                                                restString, language);
256:                                    currentLength += newLength;
257:                                }
258:                                // nothing before the tag:
259:                                else
260:                                // punctuation after the </subtree> tag:
261:                                if (restString.substring(subtreeEnd + 10,
262:                                        subtreeEnd + 11).trim().length() > 0) {
263:                                    if (logger.isLoggable(Level.FINER)) {
264:                                        logger
265:                                                .finer("PUNCTUATION AFTER THE </subtree> TAG"
266:                                                        + "/n"
267:                                                        + "STRING: "
268:                                                        + restString);
269:                                    }
270:                                    //cutting the tag first!:
271:                                    if (subtreeEnd > 0) {
272:                                        restString = removeSubTreeTag(
273:                                                restString, subtreeEnd - 1,
274:                                                subtreeEnd + 9);
275:                                    } else {
276:                                        restString = removeSubTreeTag(
277:                                                restString, subtreeEnd,
278:                                                subtreeEnd + 9);
279:                                    }
280:                                    if (logger.isLoggable(Level.FINER)) {
281:                                        logger
282:                                                .finer("STRING after cutting the </subtree> tag: "
283:                                                        + restString);
284:                                    }
285:                                    // cutting the space in the last registered component:
286:                                    if (this .htmlOutputVector.size() > 0) {
287:                                        ((MarkedArea) this .htmlOutputVector
288:                                                .elementAt(this .htmlOutputVector
289:                                                        .size() - 1)).end -= 1;
290:                                        if (currentLength > 0) {
291:                                            currentLength -= 1;
292:                                        }
293:                                    }
294:                                    if (logger.isLoggable(Level.FINER)) {
295:                                        logger.finer("currentLength: "
296:                                                + currentLength);
297:                                    }
298:                                    // register the punctuation:
299:                                    if (this .currentPosition.size() > 0) {
300:                                        newLength = register(
301:                                                currentLength,
302:                                                currentLength + 2,
303:                                                (LinPosition) this .currentPosition
304:                                                        .elementAt(this .currentPosition
305:                                                                .size() - 1),
306:                                                restString, language);
307:                                    } else {
308:                                        newLength = register(currentLength,
309:                                                currentLength + 2,
310:                                                new LinPosition("[]", true),
311:                                                restString, language);
312:                                    }
313:                                    currentLength += newLength;
314:                                } else {
315:                                    // just cutting the </subtree> tag:
316:                                    restString = removeSubTreeTag(restString,
317:                                            subtreeEnd, subtreeEnd + 10);
318:                                }
319:                            }
320:                            subtreeEnd = Utils.indexOfNotEscaped(restString,
321:                                    "</subtree");
322:                            subtreeBegin = Utils.indexOfNotEscaped(restString,
323:                                    "<subtree");
324:                            //          if (debug2) 
325:                            //                System.out.println("/subtree index: "+l2 + "<subtree"+l);
326:                            if (logger.isLoggable(Level.FINER)) {
327:                                logger.finer("<-POSITION: " + subtreeBegin
328:                                        + " CURRLENGTH: " + currentLength
329:                                        + "\n STRING: "
330:                                        + restString.substring(currentLength));
331:                            }
332:                        } //while
333:                    } else { //no focus, no selection enabled (why ever)
334:                        //that means, that all subtree tags are removed here.
335:                        if (logger.isLoggable(Level.FINER)) {
336:                            logger
337:                                    .finer("NO SELECTION IN THE TEXT TO BE APPENDED!");
338:                        }
339:                        //cutting tags from previous focuses if any:
340:                        int r = Utils.indexOfNotEscaped(restString,
341:                                "</subtree>");
342:                        while (r > -1) {
343:                            // check if punktualtion marks like . ! ? are at the end of a sentence:
344:                            if (restString.charAt(r + 10) == ' ')
345:                                restString = restString.substring(0, r)
346:                                        + restString.substring(r + 11);
347:                            else
348:                                restString = restString.substring(0, r)
349:                                        + restString.substring(r + 10);
350:                            r = Utils.indexOfNotEscaped(restString,
351:                                    "</subtree>");
352:                        }
353:                        r = Utils.indexOfNotEscaped(restString, "<subtree");
354:                        while (r > -1) {
355:                            int t = Utils.indexOfNotEscaped(restString, ">", r);
356:                            if (t < restString.length() - 2)
357:                                restString = restString.substring(0, r)
358:                                        + restString.substring(t + 2);
359:                            else
360:                                restString = restString.substring(0, r);
361:                            r = Utils.indexOfNotEscaped(restString, "<subtree");
362:                        }
363:                    }
364:                    // appending:
365:                    restString = unescapeTextFromGF(restString);
366:                    if (logger.isLoggable(Level.FINER)) {
367:                        logger.finer(restString);
368:                    }
369:                    appendedPureText = restString.replaceAll("&-", "\n ");
370:                    //display the text if not already done in case of clickable
371:                    if (!clickable && doDisplay) {
372:                        // the text has only been pruned from markup, but still needs
373:                        // to be displayed
374:                        this .display.addToStages(appendedPureText,
375:                                appendedPureText);
376:                    }
377:                } // else: nothing to append
378:                return appendedPureText;
379:            }
380:
381:            /**
382:             * Replaces a number of escaped characters by an unescaped version
383:             * of the same length
384:             * @param string The String with '\' as the escape character
385:             * @return the same String, but with escaped characters removed
386:             * 
387:             */
388:            static String unescapeTextFromGF(String string) {
389:                final String more = "\\" + ">";
390:                final String less = "\\" + "<";
391:                //%% by daniels, linearization output will be changed drastically 
392:                //(or probably will), so for now some hacks for -> and >=
393:                string = Utils.replaceAll(string, "-" + more, "-> ");
394:                string = Utils.replaceAll(string, "-" + more, "-> ");
395:                string = Utils.replaceAll(string, more, " >");
396:                string = Utils.replaceAll(string, less, " <");
397:                //an escaped \ becomes a single \
398:                string = Utils.replaceAll(string, "\\\\", " \\");
399:                return string;
400:            }
401:
402:            /**
403:             * The substring from start to end in workingString, together with
404:             * position is saved as a MarkedArea in this.htmlOutputVector.
405:             * The information from where to where the to be created MarkedArea
406:             * extends, is calculated in this method.
407:             * @param start The position of the first character in workingString
408:             * of the part, that is to be registered.
409:             * @param end The position of the last character in workingString
410:             * of the part, that is to be registered.
411:             * @param position the position in the tree that corresponds to
412:             * the to be registered text
413:             * @param workingString the String from which the displayed
414:             * characters are taken from
415:             * @param language the current linearization language
416:             * @return newLength, the difference between end and start
417:             */
418:            private int register(int start, int end, LinPosition position,
419:                    String workingString, String language) {
420:                /**
421:                 * the length of the piece of text that is to be appended now
422:                 */
423:                final int newLength = end - start;
424:                // the tag has some words to register:
425:                if (newLength > 0) {
426:                    final String stringToAppend = workingString.substring(
427:                            start, end);
428:                    //if (stringToAppend.trim().length()>0) {
429:
430:                    //get oldLength and add the new text
431:                    String toAdd = unescapeTextFromGF(stringToAppend);
432:                    final MarkedArea hma = this .display.addAsMarked(toAdd,
433:                            position, language);
434:                    this .htmlOutputVector.add(hma);
435:                    if (logger.isLoggable(Level.FINER)) {
436:                        logger.finer("HTML added  :      " + hma);
437:                    }
438:                } //some words to register
439:                return newLength;
440:            }
441:
442:            /**
443:             * removing subtree-tag in the interval start-end 
444:             * and updating the coordinates after that
445:             * basically part of appendMarked
446:             * No subtree is removed, just the tag. 
447:             * @param s The String in which the subtree tag should be removed
448:             * @param start position in restString
449:             * @param end position in restString
450:             * @return the String without the subtree-tags in the given interval
451:             */
452:            private String removeSubTreeTag(final String s, final int start,
453:                    final int end) {
454:                String restString = s;
455:                if (logger.isLoggable(Level.FINER)) {
456:                    logger.finer("removing: " + start + " to " + end);
457:                }
458:                int difference = end - start + 1;
459:                int positionStart, positionEnd;
460:                if (difference > 20) {
461:                    positionStart = Utils.indexOfNotEscaped(restString, "[",
462:                            start);
463:                    positionEnd = Utils.indexOfNotEscaped(restString, "]",
464:                            start);
465:
466:                    currentPosition.addElement(new LinPosition(restString
467:                            .substring(positionStart, positionEnd + 1),
468:                            restString.substring(start, end).indexOf(
469:                                    "incorrect") == -1));
470:                } else if (currentPosition.size() > 0) {
471:                    currentPosition.removeElementAt(currentPosition.size() - 1);
472:                }
473:                if (start > 0) {
474:                    restString = restString.substring(0, start)
475:                            + restString.substring(end + 1);
476:                } else {
477:                    restString = restString.substring(end + 1);
478:                }
479:                return restString;
480:            }
481:
482:            /**
483:             * Goes through the list of MarkedAreas and creates MarkedAreaHighlightingStatus
484:             * objects for them, which contain fields for incorrect constraints
485:             * and if they belong to the selected subtree.
486:             * @param focusPosition The AST position of the selected node
487:             * @return a Vector of MarkedAreaHighlightingStatus
488:             */
489:            Vector calculateHighlights(LinPosition focusPosition) {
490:                Vector result = new Vector();
491:                final HashSet incorrectMA = new HashSet();
492:                for (int i = 0; i < htmlOutputVector.size(); i++) {
493:                    final MarkedArea ma = (MarkedArea) this .htmlOutputVector
494:                            .elementAt(i);
495:                    //check, if and how ma should be highlighted
496:                    boolean incorrect = false;
497:                    boolean focused = false;
498:                    if (logger.isLoggable(Level.FINER)) {
499:                        logger.finer("Highlighting: " + ma);
500:                    }
501:                    if (!ma.position.correctPosition) {
502:                        incorrectMA.add(ma);
503:                        incorrect = true;
504:                    } else {
505:                        //This could be quadratic, but normally on very
506:                        //few nodes constraints are introduced, so
507:                        //incorrectMA should not contain many elements.
508:                        MarkedArea incMA;
509:                        for (Iterator it = incorrectMA.iterator(); !incorrect
510:                                && it.hasNext();) {
511:                            incMA = (MarkedArea) it.next();
512:                            if (LinPosition.isSubtreePosition(incMA.position,
513:                                    ma.position)) {
514:                                incorrect = true;
515:                            }
516:                        }
517:                    }
518:                    if (LinPosition.isSubtreePosition(focusPosition,
519:                            ma.position)) {
520:                        focused = true;
521:                    }
522:                    MarkedAreaHighlightingStatus mahs = new MarkedAreaHighlightingStatus(
523:                            focused, incorrect, ma);
524:                    result.add(mahs);
525:                }
526:                return result;
527:            }
528:
529:            /**
530:             * Parses the linearization XML and calls outputAppend
531:             * @param langMan The LangMenuModel, but that is an inner class and only
532:             * the methods in the Interface LanguageManager are used here.
533:             */
534:            void parseLin(LanguageManager langMan) {
535:                linearizations.clear();
536:                boolean firstLin = true;
537:                //read first line like '    <lin lang=Abstract>'
538:                String readResult = linearization.substring(0, linearization
539:                        .indexOf('\n'));
540:                //the rest of the linearizations
541:                String lin = linearization.substring(linearization
542:                        .indexOf('\n') + 1);
543:                //extract the language from readResult
544:                int ind = Utils.indexOfNotEscaped(readResult, "=");
545:                int ind2 = Utils.indexOfNotEscaped(readResult, ">");
546:                /** The language of the linearization */
547:                String language = readResult.substring(ind + 1, ind2);
548:                //the first direct linearization
549:                readResult = lin.substring(0, lin.indexOf("</lin>"));
550:                //the rest
551:                lin = lin.substring(lin.indexOf("</lin>"));
552:                while (readResult.length() > 1) {
553:                    langMan.add(language, true);
554:                    // selected?
555:                    boolean visible = langMan.isLangActive(language);
556:                    if (visible && !firstLin) {
557:                        // appending sth. linearizationArea
558:                        this .display.addToStages("\n************\n",
559:                                "<br><hr><br>");
560:                    }
561:                    if (logger.isLoggable(Level.FINER)) {
562:                        logger.finer("linearization for the language: "
563:                                + readResult);
564:                    }
565:
566:                    // change the focus tag into a subtree tag.
567:                    // focus handling now happens in GFEditor2::formTree
568:                    String readLin = readResult;
569:                    readLin = Utils.replaceNotEscaped(readLin, "<focus",
570:                            "<subtree");
571:                    readLin = Utils.replaceNotEscaped(readLin, "</focus",
572:                            "</subtree");
573:
574:                    final boolean isAbstract = "Abstract".equals(language);
575:                    // now do appending and registering
576:                    String linResult = appendMarked(readLin + '\n',
577:                            !isAbstract, visible, language);
578:
579:                    if (visible) {
580:                        firstLin = false;
581:                    }
582:                    linearizations.put(language, linResult);
583:                    // read </lin>
584:                    lin = lin.substring(lin.indexOf('\n') + 1);
585:                    // read lin or 'end'
586:                    if (lin.length() < 1) {
587:                        break;
588:                    }
589:
590:                    readResult = lin.substring(0, lin.indexOf('\n'));
591:                    lin = lin.substring(lin.indexOf('\n') + 1);
592:                    if (readResult.indexOf("<lin ") != -1) {
593:                        //extract the language from readResult
594:                        ind = readResult.indexOf('=');
595:                        ind2 = readResult.indexOf('>');
596:                        language = readResult.substring(ind + 1, ind2);
597:                        readResult = lin.substring(0, lin.indexOf("</lin>"));
598:                        lin = lin.substring(lin.indexOf("</lin>"));
599:                    }
600:                }
601:            }
602:
603:            /**
604:             * 
605:             * @param language The concrete language of choice
606:             * @return The linearization of the subtree starting with the currently
607:             * selected node in the given language.
608:             */
609:            String getSelectedLinearization(final String language,
610:                    final LinPosition focusPosition) {
611:                StringBuffer sel = new StringBuffer();
612:                for (int i = 0; i < htmlOutputVector.size(); i++) {
613:                    final MarkedArea ma = (MarkedArea) htmlOutputVector
614:                            .elementAt(i);
615:                    if (language.equals(ma.language)
616:                            && LinPosition.isSubtreePosition(focusPosition,
617:                                    ma.position)) {
618:                        sel.append(ma.words);
619:                    }
620:                }
621:                return sel.toString();
622:            }
623:
624:            /**
625:             * Takes the index of a caret position in the linearization area
626:             * and returns the language of the clicked linearization.
627:             * GF lists the different concrete languages one after the other,
628:             * and this method looks at the linearization snipplets to get
629:             * the language.
630:             * If somehow no language can be found out, 'Abstract' is returned
631:             * @param pos The index of the caret position
632:             * @param htmlClicked If the HTML JTextPane has been clicked,
633:             * false for the JTextArea
634:             * @return the name of the concrete grammar (language) or Abstract
635:             * (see above).
636:             */
637:            String getLanguageForPos(int pos, final boolean htmlClicked) {
638:                final String language;
639:                MarkedArea ma = null;
640:                if (htmlClicked) {
641:                    //HTML
642:                    for (int i = 0; i < htmlOutputVector.size(); i++) {
643:                        if ((pos >= ((MarkedArea) htmlOutputVector.get(i)).htmlBegin)
644:                                && (pos <= ((MarkedArea) htmlOutputVector
645:                                        .get(i)).htmlEnd)) {
646:                            ma = (MarkedArea) htmlOutputVector.get(i);
647:                            break;
648:                        }
649:                    }
650:                } else {
651:                    //assumably pure text
652:                    for (int i = 0; i < htmlOutputVector.size(); i++) {
653:                        if ((pos >= ((MarkedArea) htmlOutputVector.get(i)).begin)
654:                                && (pos <= ((MarkedArea) htmlOutputVector
655:                                        .get(i)).end)) {
656:                            ma = (MarkedArea) htmlOutputVector.get(i);
657:                            break;
658:                        }
659:                    }
660:
661:                }
662:                if (ma != null && ma.language != null) {
663:                    language = ma.language;
664:                } else {
665:                    language = "Abstract";
666:                }
667:                return language;
668:            }
669:
670:            /**
671:             * The user has either just clicked in the linearization area,
672:             * which means start == end, or he has selected a text, so that 
673:             * start < end.
674:             * This method figures out the smallest subtree whose linearization
675:             * completely encompasses the area from start to end.
676:             * This method is for the HTML linearization area.
677:             * @param start The index of the caret position at the begin of the selection
678:             * @param end The index of the caret position at the end of the selection
679:             * @return The 'root' of the subtree described above
680:             */
681:            String markedAreaForPosHtml(int start, int end) {
682:                if (htmlOutputVector.isEmpty()) {
683:                    return null;
684:                }
685:                String position = null; //the result
686:                String jPosition = "", iPosition = "";
687:                MarkedArea jElement = null;
688:                MarkedArea iElement = null;
689:                int j = 0;
690:                int i = htmlOutputVector.size() - 1;
691:
692:                if (logger.isLoggable(Level.FINER))
693:                    for (int k = 0; k < htmlOutputVector.size(); k++) {
694:                        logger
695:                                .finer("element: "
696:                                        + k
697:                                        + " begin "
698:                                        + ((MarkedArea) htmlOutputVector
699:                                                .elementAt(k)).htmlBegin
700:                                        + " "
701:                                        + "\n-> end: "
702:                                        + ((MarkedArea) htmlOutputVector
703:                                                .elementAt(k)).htmlEnd
704:                                        + " "
705:                                        + "\n-> position: "
706:                                        + (((MarkedArea) htmlOutputVector
707:                                                .elementAt(k)).position).position
708:                                        + " "
709:                                        + "\n-> words: "
710:                                        + ((MarkedArea) htmlOutputVector
711:                                                .elementAt(k)).words);
712:                    }
713:                // localizing end:
714:                while ((j < htmlOutputVector.size())
715:                        && (((MarkedArea) htmlOutputVector.elementAt(j)).htmlEnd < end)) {
716:                    j++;
717:                }
718:                // localising start:
719:                while ((i >= 0)
720:                        && (((MarkedArea) htmlOutputVector.elementAt(i)).htmlBegin > start)) {
721:                    i--;
722:                }
723:                if (logger.isLoggable(Level.FINER)) {
724:                    logger.finer("i: " + i + " j: " + j);
725:                }
726:                if ((j < htmlOutputVector.size())) {
727:                    jElement = (MarkedArea) htmlOutputVector.elementAt(j);
728:                    jPosition = jElement.position.position;
729:                    // less & before:
730:                    if (i == -1) { // less:
731:                        if (end >= jElement.htmlBegin) {
732:                            iElement = (MarkedArea) htmlOutputVector
733:                                    .elementAt(0);
734:                            iPosition = iElement.position.position;
735:                            if (logger.isLoggable(Level.FINER)) {
736:                                logger.finer("Less: " + jPosition + " and "
737:                                        + iPosition);
738:                            }
739:                            position = findMax(0, j);
740:                            if (logger.isLoggable(Level.FINER)) {
741:                                logger
742:                                        .finer("SELECTEDTEXT: " + position
743:                                                + "\n");
744:                            }
745:                        } else { // before: 
746:                            if (logger.isLoggable(Level.FINER)) {
747:                                logger.finer("BEFORE vector of size: "
748:                                        + htmlOutputVector.size());
749:                            }
750:                        }
751:                    } else { // just: 
752:                        iElement = (MarkedArea) htmlOutputVector.elementAt(i);
753:                        iPosition = iElement.position.position;
754:                        if (logger.isLoggable(Level.FINER)) {
755:                            logger.finer("SELECTED TEXT Just: " + iPosition
756:                                    + " and " + jPosition + "\n");
757:                        }
758:                        position = findMax(i, j);
759:                        if (logger.isLoggable(Level.FINER)) {
760:                            logger.finer("SELECTEDTEXT: " + position + "\n");
761:                        }
762:                    }
763:                } else if (i >= 0) { // more && after:
764:                    iElement = (MarkedArea) htmlOutputVector.elementAt(i);
765:                    iPosition = iElement.position.position;
766:                    // more
767:                    if (start <= iElement.htmlEnd) {
768:                        jElement = (MarkedArea) htmlOutputVector
769:                                .elementAt(htmlOutputVector.size() - 1);
770:                        jPosition = jElement.position.position;
771:                        if (logger.isLoggable(Level.FINER)) {
772:                            logger.finer("MORE: " + iPosition + " and "
773:                                    + jPosition);
774:                        }
775:                        position = findMax(i, htmlOutputVector.size() - 1);
776:                        if (logger.isLoggable(Level.FINER)) {
777:                            logger.finer("SELECTEDTEXT: " + position + "\n");
778:                        }
779:                        // after:
780:                    } else if (logger.isLoggable(Level.FINER)) {
781:                        logger.finer("AFTER vector of size: "
782:                                + htmlOutputVector.size());
783:                    }
784:                } else { // bigger:
785:                    iElement = (MarkedArea) htmlOutputVector.elementAt(0);
786:                    iPosition = iElement.position.position;
787:                    jElement = (MarkedArea) htmlOutputVector
788:                            .elementAt(htmlOutputVector.size() - 1);
789:                    jPosition = jElement.position.position;
790:                    if (logger.isLoggable(Level.FINER)) {
791:                        logger.finer("BIGGER: " + iPosition + " and "
792:                                + jPosition + "\n" + "\n-> SELECTEDTEXT: []\n");
793:                    }
794:                    position = "[]";
795:                }
796:                return position;
797:            }
798:
799:            /**
800:             * The user has either just clicked in the linearization area,
801:             * which means start == end, or he has selected a text, so that 
802:             * start < end.
803:             * This method figures out the smallest subtree whose linearization
804:             * completely encompasses the area from start to end.
805:             * This method is for the pure text linearization area.
806:             * @param start The index of the caret position at the begin of the selection
807:             * @param end The index of the caret position at the end of the selection
808:             * @return The 'root' of the subtree described above
809:             */
810:            String markedAreaForPosPureText(int start, int end) {
811:                if (htmlOutputVector.isEmpty()) {
812:                    return null;
813:                }
814:                //the result
815:                String position = null;
816:                //variables for confining the searched MarkedArea from 
817:                //start and end (somehow ...)
818:                int j = 0;
819:                int i = htmlOutputVector.size() - 1;
820:                String jPosition = "", iPosition = "";
821:                MarkedArea jElement = null;
822:                MarkedArea iElement = null;
823:
824:                if (logger.isLoggable(Level.FINER))
825:                    for (int k = 0; k < htmlOutputVector.size(); k++) {
826:                        logger
827:                                .finer("element: "
828:                                        + k
829:                                        + " begin "
830:                                        + ((MarkedArea) htmlOutputVector
831:                                                .elementAt(k)).begin
832:                                        + " "
833:                                        + "\n-> end: "
834:                                        + ((MarkedArea) htmlOutputVector
835:                                                .elementAt(k)).end
836:                                        + " "
837:                                        + "\n-> position: "
838:                                        + (((MarkedArea) htmlOutputVector
839:                                                .elementAt(k)).position).position
840:                                        + " "
841:                                        + "\n-> words: "
842:                                        + ((MarkedArea) htmlOutputVector
843:                                                .elementAt(k)).words);
844:                    }
845:                // localizing end:
846:                while ((j < htmlOutputVector.size())
847:                        && (((MarkedArea) htmlOutputVector.elementAt(j)).end < end)) {
848:                    j++;
849:                }
850:                // localising start:
851:                while ((i >= 0)
852:                        && (((MarkedArea) htmlOutputVector.elementAt(i)).begin > start))
853:                    i--;
854:                if (logger.isLoggable(Level.FINER)) {
855:                    logger.finer("i: " + i + " j: " + j);
856:                }
857:                if ((j < htmlOutputVector.size())) {
858:                    jElement = (MarkedArea) htmlOutputVector.elementAt(j);
859:                    jPosition = jElement.position.position;
860:                    // less & before:
861:                    if (i == -1) { // less:
862:                        if (end >= jElement.begin) {
863:                            iElement = (MarkedArea) htmlOutputVector
864:                                    .elementAt(0);
865:                            iPosition = iElement.position.position;
866:                            if (logger.isLoggable(Level.FINER)) {
867:                                logger.finer("Less: " + jPosition + " and "
868:                                        + iPosition);
869:                            }
870:                            position = findMax(0, j);
871:                            if (logger.isLoggable(Level.FINER)) {
872:                                logger
873:                                        .finer("SELECTEDTEXT: " + position
874:                                                + "\n");
875:                            }
876:                        } else if (logger.isLoggable(Level.FINER)) { // before: 
877:                            logger.finer("BEFORE vector of size: "
878:                                    + htmlOutputVector.size());
879:                        }
880:                    } else { // just: 
881:                        iElement = (MarkedArea) htmlOutputVector.elementAt(i);
882:                        iPosition = iElement.position.position;
883:                        if (logger.isLoggable(Level.FINER)) {
884:                            logger.finer("SELECTED TEXT Just: " + iPosition
885:                                    + " and " + jPosition + "\n");
886:                        }
887:                        position = findMax(i, j);
888:                        if (logger.isLoggable(Level.FINER)) {
889:                            logger.finer("SELECTEDTEXT: " + position + "\n");
890:                        }
891:                    }
892:                } else if (i >= 0) { // more && after:
893:                    iElement = (MarkedArea) htmlOutputVector.elementAt(i);
894:                    iPosition = iElement.position.position;
895:                    // more
896:                    if (start <= iElement.end) {
897:                        jElement = (MarkedArea) htmlOutputVector
898:                                .elementAt(htmlOutputVector.size() - 1);
899:                        jPosition = jElement.position.position;
900:                        if (logger.isLoggable(Level.FINER)) {
901:                            logger.finer("MORE: " + iPosition + " and "
902:                                    + jPosition);
903:                        }
904:                        position = findMax(i, htmlOutputVector.size() - 1);
905:                        if (logger.isLoggable(Level.FINER)) {
906:                            logger.finer("SELECTEDTEXT: " + position + "\n");
907:                        }
908:                    } else if (logger.isLoggable(Level.FINER)) { // after: 
909:                        logger.finer("AFTER vector of size: "
910:                                + htmlOutputVector.size());
911:                    }
912:                } else {
913:                    // bigger:
914:                    iElement = (MarkedArea) htmlOutputVector.elementAt(0);
915:                    iPosition = iElement.position.position;
916:                    jElement = (MarkedArea) htmlOutputVector
917:                            .elementAt(htmlOutputVector.size() - 1);
918:                    jPosition = jElement.position.position;
919:                    if (logger.isLoggable(Level.FINER)) {
920:                        logger.finer("BIGGER: " + iPosition + " and "
921:                                + jPosition + "\n" + "\n-> SELECTEDTEXT: []\n");
922:                    }
923:                    position = "[]";
924:                }
925:                return position;
926:            }
927:
928:        }
www.java2java.com | Contact Us
Copyright 2009 - 12 Demo Source and Support. All rights reserved.
All other trademarks are property of their respective owners.