← Back to branch summary

~ubuntu-branches/ubuntu/maverick/electric/maverick

« back to all changes in this revision

Viewing changes to com/sun/electric/tool/user/help/ManualViewer.java

  • Committer: Bazaar Package Importer
  • Author(s): Onkar Shinde
  • Date: 2010-01-09 16:26:04 UTC
  • mfrom: (1.1.4 upstream) (3.1.6 sid)
  • Revision ID: james.westby@ubuntu.com-20100109162604-1ypvmy8ijmlc6oq7
Tags: 8.10-1
* New upstream version.
* debian/control
  - Add libjava3d-java and quilt build dependencies.
  - Update standards version to 3.8.3.
  - Add libjava3d-java as recommends to binary package.
* debian/rules
  - Use quilt patch system instead of simple patchsys.
  - Add java3d related jar files to DEB_JARS.
* debian/patches/*
  - Update as per current upstream source. Convert to quilt.
* debian/ant.properties
  - Do not disable 3D plugin anymore.
  - Use new property to disable compilation of OS X related classes.
* debian/wrappers/electric
  - Add java3d related jar files to runtime classpath.
* debian/README.source
  - Change text to the appropriate one for quilt.

Show diffs side-by-side

added added

removed removed

Lines of Context:
com/sun/electric/tool/user/help/ManualViewer.java
121
121
                excludeMenu.add("Sun");
122
122
                excludeMenu.add("Test");
123
123
                excludeMenu.add("Steve");
124
 
                excludeMenu.add("Russell");
125
124
                excludeMenu.add("JonG");
126
125
                excludeMenu.add("Gilda");
127
126
                excludeMenu.add("Dima");
128
 
                excludeMenu.add("Kon");
 
127
                excludeMenu.add("Dinesh");
129
128
                excludeMenu.add("Frankie");
130
 
                excludeMenu.add("Dinesh");
131
 
                excludeMenu.add("Eric");
 
129
                excludeMenu.add("Adam");
132
130
        }
133
131
 
134
132
        private static class PageInfo
181
179
        if (theManual != null && setVisible)
182
180
            theManual.setVisible(true);
183
181
    }
184
 
    
 
182
 
185
183
    /**
186
184
         * Method to display the user's manual.
187
185
         */
240
238
                    PageInfo pi = theManual.pageSequence.get(i);
241
239
                    if (pi.fileName.equals(prefFileName))
242
240
                    {
243
 
                        theManual.loadPage(i);
 
241
                        theManual.loadPage(i, null);
244
242
                        break;
245
243
                    }
246
244
                }
292
290
                for (Iterator<NodeInst> it = cell.getNodes(); it.hasNext();)
293
291
                {
294
292
                        NodeInst ni = it.next();
295
 
                        ni.setExpanded();
 
293
                        ni.setExpanded(true);
296
294
                }
297
295
 
298
296
                // to guarantee the redisplay with extended
474
472
                        manualTree.setSelectionPath(tp);
475
473
                }
476
474
                // load the title page of the manual
477
 
                loadPage(currentIndex);
 
475
                loadPage(currentIndex, null);
478
476
                finishInitialization();
479
477
        }
480
478
 
736
734
                                PageInfo pi = dialog.pageSequence.get(i);
737
735
                                if (pi.fileName.equals(fileName))
738
736
                                {
739
 
                                        dialog.loadPage(i);
 
737
                                        dialog.loadPage(i, null);
740
738
                                        return;
741
739
                                }
742
740
                        }
760
758
                return sb.toString();
761
759
        }
762
760
 
763
 
        private void loadPage(int index)
 
761
        private void loadPage(int index, String highlightThis)
764
762
        {
765
763
                // add to browsing history
766
764
                history.add(new Integer(index));
782
780
                }
783
781
                StringBuffer sb = new StringBuffer();
784
782
 
 
783
                // setup for search
 
784
                Pattern pattern = null;
 
785
                if (highlightThis != null) pattern = Pattern.compile(highlightThis, Pattern.CASE_INSENSITIVE);
 
786
 
785
787
                // emit header HTML
786
788
                sb.append("<BASE href=\"" + pi.url.toString() + "\">");
787
789
 
827
829
                                sb.append("</HTML>\n");
828
830
                                continue;
829
831
                        }
 
832
 
 
833
                        if (pattern != null)
 
834
                        {
 
835
                                StringBuffer oneLine = new StringBuffer();
 
836
                                Matcher matcher = pattern.matcher(line);
 
837
                                while (matcher.find())
 
838
                                        matcher.appendReplacement(oneLine, "<FONT style=\"BACKGROUND-COLOR: red\">" + highlightThis + "</FONT>");
 
839
                                matcher.appendTail(oneLine);
 
840
                                line = oneLine.toString();
 
841
                        }
830
842
                        sb.append(line);
831
843
                        sb.append("\n");
832
844
                }
855
867
                {
856
868
                        history.remove(len-2);
857
869
                        Integer lpi = (Integer)lastPage;
858
 
                        loadPage(lpi.intValue());
 
870
                        loadPage(lpi.intValue(), null);
859
871
                        return;
860
872
                }
861
873
                if (lastPage instanceof String)
872
884
        {
873
885
                int index = currentIndex - 1;
874
886
                if (index < 0) index = pageSequence.size() - 1;
875
 
                loadPage(index);
 
887
                loadPage(index, null);
876
888
        }
877
889
 
878
890
        /**
882
894
        {
883
895
                int index = currentIndex + 1;
884
896
                if (index >= pageSequence.size()) index = 0;
885
 
                loadPage(index);
 
897
                loadPage(index, null);
886
898
        }
887
899
 
888
900
        private void search()
893
905
 
894
906
                StringBuffer sbResult = new StringBuffer();
895
907
 
896
 
                sbResult.append("<CENTER><H1>Search Results for " + ret + "</H1></CENTER>\n");
 
908
                sbResult.append("<CENTER><H1>Search Results for \"" + ret + "\"</H1></CENTER>\n");
897
909
                int numFound = 0;
898
910
                for(int index=0; index < pageSequence.size(); index++)
899
911
                {
914
926
                        }
915
927
                        Matcher matcher = pattern.matcher(sb.toString());
916
928
                        if (!matcher.find()) continue;
917
 
                        sbResult.append("<B><A HREF=\"" + pi.fileName + ".html\">" + pi.fullChapterNumber + ": " + pi.title + "</A></B<BR>\n");
 
929
                        sbResult.append("<B><A HREF=\"" + pi.fileName + ".html##" + ret + "\">" + pi.fullChapterNumber + ": " + pi.title + "</A></B><BR>\n");
918
930
                        numFound++;
919
931
                }
920
932
                sbResult.append("<P><B>Found " + numFound + " entries</B>\n");
994
1006
                                                                String prefix = pageName.substring(0, secondDash) + ": ";
995
1007
                                                                printWriter.println("<CENTER><H2>" + prefix + pi.outerChapterTitle + "</H2></CENTER>");
996
1008
                                                                printWriter.println("<HR>");
997
 
                                                                printWriter.println("<BR>");                                                            
 
1009
                                                                printWriter.println("<BR>");
998
1010
                                                        }
999
1011
                                                }
1000
1012
                                        }
1231
1243
                                                        int firstDash = pageName.indexOf('-');
1232
1244
                                                        int secondDash = pageName.indexOf('-', firstDash+1);
1233
1245
                                                        String prefix = pageName.substring(0, secondDash) + ": ";
1234
 
                                                        intermediateTitle = prefix + pi.outerChapterTitle;                                                      
 
1246
                                                        intermediateTitle = prefix + pi.outerChapterTitle;
1235
1247
                                                }
1236
1248
                                        }
1237
1249
 
1311
1323
                dialog.setVisible(true);
1312
1324
        }
1313
1325
 
1314
 
        private static class EditHTML extends EModelessDialog
 
1326
        public static class EditHTML extends EModelessDialog
1315
1327
        {
1316
1328
                private JTextArea textArea;
1317
1329
                private URL file;
1412
1424
 
1413
1425
                        setVisible(false);
1414
1426
                        dispose();
1415
 
                        world.loadPage(world.currentIndex);
 
1427
                        world.loadPage(world.currentIndex, null);
1416
1428
                }
1417
1429
        }
1418
1430
 
1438
1450
 
1439
1451
                                        // first see if it is one of the manual files, in which case it gets auto-generated
1440
1452
                                        String desiredFile = desiredURL.getFile();
 
1453
                                        String searchString = desiredURL.getRef();
 
1454
                                        if (searchString != null && searchString.startsWith("#")) searchString = searchString.substring(1); else
 
1455
                                                searchString = null;
1441
1456
                                        for(int i=0; i<dialog.pageSequence.size(); i++)
1442
1457
                                        {
1443
1458
                                                PageInfo pi = dialog.pageSequence.get(i);
1444
1459
                                                if (pi.url.getFile().equals(desiredFile))
1445
1460
                                                {
1446
 
                                                        dialog.loadPage(i);
 
1461
                                                        dialog.loadPage(i, searchString);
1447
1462
                                                        return;
1448
1463
                                                }
1449
1464
                                        }
1694
1709
                        if (obj instanceof Integer)
1695
1710
                        {
1696
1711
                                int index = ((Integer)obj).intValue();
1697
 
                                dialog.loadPage(index);
 
1712
                                dialog.loadPage(index, null);
1698
1713
                        }
1699
1714
                }
1700
1715
        }