Back to index

wims  3.65+svn20090927
TextDisplay.java
Go to the documentation of this file.
00001 package rene.viewer;
00002 
00003 import java.io.*;
00004 import java.awt.*;
00005 import java.awt.datatransfer.*;
00006 import java.awt.event.*;
00007 
00008 import rene.util.list.*;
00009 import rene.gui.*;
00010 
00011 class ClipboardCopy extends Thread
00012 {      String S;
00013        ClipboardOwner C;
00014        Canvas Cv;
00015        public ClipboardCopy (ClipboardOwner c, Canvas cv, String s)
00016        {      S=s; C=c; Cv=cv;
00017               start();
00018        }
00019        public void run ()
00020        {      Clipboard clip=Cv.getToolkit().getSystemClipboard();
00021               StringSelection cont=new StringSelection(S);
00022               clip.setContents(cont,C);
00023        }
00024 }
00025 
00026 public class TextDisplay extends Canvas 
00027        implements ClipboardOwner, ComponentListener
00028 {      ListClass L;
00029        Font F=null;
00030        FontMetrics FM;
00031        Viewer V;
00032        int Leading,Height,Ascent,Descent;
00033        int LineCount,TopLineCount;
00034        int PageSize;
00035        ListElement TopLine;
00036        Image I;
00037        Graphics IG;
00038        int W,H;
00039        public int Tabsize=4;
00040        public int Offset;
00041        boolean LineFinished=true;
00042        int Widths[],HW[];
00043        long LastScrollTime;
00044        Color Background;
00045        int TabWidth=0;
00046 
00047        public TextDisplay (Viewer v)
00048        {      L=new ListClass();
00049               F=null;
00050               V=v;
00051               LineCount=0;
00052               TopLineCount=0;
00053               TopLine=null;
00054               I=null;
00055               W=H=0;
00056               PageSize=10;
00057               HW=new int[1024];
00058               addKeyListener(v);
00059               addComponentListener(this);
00060        }
00061 
00062        void init (Font f)
00063        {      F=f;
00064               FM=getFontMetrics(F);
00065               Leading=FM.getLeading()+Global.getParameter("fixedfont.spacing",-1);
00066               Height=FM.getHeight();
00067               Ascent=FM.getAscent();
00068               Descent=FM.getDescent();
00069               Widths=FM.getWidths();
00070               if (Global.Background!=null) Background=Global.Background;
00071               else Background=SystemColor.window;
00072        }
00073 
00074        public Color getBackground ()
00075        {      if (Global.Background!=null) return Global.Background;
00076               else return SystemColor.window;
00077        }
00078 
00079        int [] getwidth (char a[])
00080        {      try
00081               {      for (int i=0; i<a.length; i++)
00082                      {      if (a[i]<256) HW[i]=Widths[a[i]];
00083                             else HW[i]=FM.charWidth(a[i]);
00084                      }
00085               }
00086               catch (Exception e) { return HW; }
00087               return HW;
00088        }
00089 
00090        public synchronized void appendLine0 (String S)
00091        {      appendLine0(S,Color.black);
00092        }
00093 
00094        public synchronized void appendLine0 (String S, Color c)
00095        {      Line l;
00096               L.append(new ListElement(l=new Line(S,this,c)));
00097               LineCount++;
00098               if (LineCount==1) TopLine=L.first();
00099               LineFinished=true;
00100               if (TabWidth>0) l.expandTabs(TabWidth);
00101        }
00102 
00103        public synchronized void appendLine (String s)
00104        {      appendLine0(s);
00105               V.setVerticalScrollbar();
00106        }
00107 
00108        public void append (String S, Color c)
00109        {      append(S,c,true);
00110        }
00111 
00112        public void append (String S, Color c, boolean suddenupdate)
00113        {      while (true)
00114               {      int p=S.indexOf('\n');
00115                      if (p<0)
00116                      {      appendlast(S,c);
00117                             LineFinished=false;
00118                             break;
00119                      }
00120                      appendlast(S.substring(0,p),c);
00121                      LineFinished=true;
00122                      S=S.substring(p+1);
00123                      if (S.equals("")) 
00124                      {      break;
00125                      }
00126               }
00127               if (suddenupdate) doUpdate(true);
00128               repaint();
00129        }
00130 
00131        public void doUpdate (boolean showlast)
00132        {      if (showlast)
00133               {      long m=System.currentTimeMillis();
00134                      if (m-LastScrollTime > 10000) showlast();
00135               }
00136               repaint();
00137               V.setVerticalScrollbar();
00138        }
00139 
00140        public void setText (String s)
00141        {      TopLine=null; TopLineCount=0; LineCount=0;
00142               L=new ListClass();
00143               if (!s.equals("")) append(s,Color.black);
00144               repaint();
00145        }
00146 
00147        public synchronized void appendlast (String s, Color c)
00148        {      if (LineFinished || L.last()==null)
00149               {      Line l;
00150                      L.append(new ListElement(l=new Line(s,this,c)));
00151                      LineCount++;
00152                      if (LineCount==1) TopLine=L.first();
00153                      if (TabWidth>0) l.expandTabs(TabWidth);
00154               }
00155               else
00156               {      ((Line)L.last().content()).append(s);
00157               }
00158        }
00159 
00160        public void showlast ()
00161        {      ListElement e=L.last();
00162               if (e==null) return;
00163               TopLineCount=LineCount;
00164               for (int i=0; i<PageSize-1; i++)
00165               {      if (e.previous()==null) break;
00166                      e=e.previous();
00167                      TopLineCount--;
00168               }
00169               TopLine=e;
00170               repaint();
00171        }
00172 
00173        public void makeimage ()
00174        {      Dimension D=getSize();
00175               if (I==null || D.width!=W || D.height!=H)
00176               {      I=createImage(W=D.width,H=D.height);
00177                      IG=I.getGraphics();
00178               }
00179               IG.setColor(Color.black);
00180               IG.clearRect(0,0,W,H);
00181               IG.setFont(F);
00182               try
00183               {      PageSize=H/(Height+Leading);
00184               }
00185               catch (Exception e) {}
00186        }
00187 
00188        public synchronized void paint (Graphics g)
00189        {      if (F==null) init(getFont());
00190               makeimage();
00191               ListElement e=TopLine;
00192               antialias(true);
00193               int h=Leading+Ascent;
00194               int totalh=getSize().height-Descent;
00195               if (Background==null) Background=getBackground();
00196               IG.setColor(Background);
00197               IG.fillRect(0,0,W,H);
00198               int lines=0;
00199               while (lines<PageSize && e!=null)
00200               {      Line l=(Line)e.content();
00201                      l.draw(IG,2,h);
00202                      h+=Leading+Height;
00203                      e=e.next();
00204                      lines++;
00205               }
00206               g.drawImage(I,0,0,this);
00207        }
00208 
00214        public void antialias (boolean flag)
00215        {      if (Global.getParameter("font.smooth",true))
00216               {      IG=(Graphics2D)IG;
00217                      ((Graphics2D)IG).setRenderingHint(RenderingHints.KEY_TEXT_ANTIALIASING,
00218                             flag?RenderingHints.VALUE_TEXT_ANTIALIAS_ON:
00219                                    RenderingHints.VALUE_TEXT_ANTIALIAS_OFF);
00220               }
00221        }
00222        
00223        public void showLine (ListElement line)
00224        {      ListElement e=TopLine;
00225               int h=Leading+Ascent;
00226               int totalh=getSize().height-Descent;
00227               if (Background==null) Background=getBackground();
00228               int lines=0;
00229               while (lines<PageSize && e!=null)
00230               {      if (e==line) return;
00231                      h+=Leading+Height;
00232                      e=e.next();
00233                      lines++;
00234               }
00235               if (e==line && TopLine.next()!=null) 
00236                      TopLine=TopLine.next();
00237               else TopLine=line;
00238        }
00239 
00240        public ListElement getline (int y)
00241        {      if (TopLine==null) return null;
00242               ListElement e=TopLine;
00243               int h=Leading+Height;
00244               if (h==0) return null;
00245               h=y/h;
00246               for (int i=0; i<h; i++)
00247               {      if (e.next()==null) return e;
00248                      e=e.next();
00249               }
00250               return e;
00251        }
00252 
00253        public void update (Graphics g)
00254        {      paint(g);
00255        }
00256 
00257        int computeVertical ()
00258        {      if (LineCount>0)
00259                return TopLineCount*1000/LineCount;
00260            else return 0;
00261        }
00262 
00263        public int setVertical (int v)
00264        {      if (TopLine==null) return 0;
00265               int NewTop=LineCount*v/1000;
00266               if (NewTop>TopLineCount)
00267               {      for (int i=TopLineCount; i<NewTop; i++)
00268                      {      if (TopLine.next()==null) break;
00269                             TopLine=TopLine.next();
00270                             TopLineCount++;
00271                      }
00272                      repaint();
00273               }
00274               else if (NewTop<TopLineCount)
00275               {      for (int i=TopLineCount; i>NewTop; i--)
00276                      {      if (TopLine.previous()==null) break;
00277                             TopLine=TopLine.previous();
00278                             TopLineCount--;
00279                      }
00280                      repaint();
00281               }
00282               LastScrollTime=System.currentTimeMillis();
00283               return v;
00284        }
00285 
00286        public void verticalUp ()
00287        {      if (TopLine==null) return;
00288               if (TopLine.next()==null) return;
00289               TopLine=TopLine.next();
00290               TopLineCount++;
00291               repaint();
00292               LastScrollTime=System.currentTimeMillis();
00293        }
00294 
00295        public void verticalDown ()
00296        {      if (TopLine==null) return;
00297               if (TopLine.previous()==null) return;
00298               TopLine=TopLine.previous();
00299               TopLineCount--;
00300               repaint();
00301               LastScrollTime=System.currentTimeMillis();
00302        }
00303 
00304        public void verticalPageUp ()
00305        {      if (TopLine==null) return;
00306               for (int i=0; i<PageSize-1; i++)
00307               {      if (TopLine.next()==null) break;
00308                      TopLine=TopLine.next();
00309                      TopLineCount++;
00310               }
00311               repaint();
00312               LastScrollTime=System.currentTimeMillis();
00313        }
00314 
00315        public void verticalPageDown ()
00316        {      if (TopLine==null) return;
00317               for (int i=0; i<PageSize-1; i++)
00318               {      if (TopLine.previous()==null) break;
00319                      TopLine=TopLine.previous();
00320                      TopLineCount--;
00321               }
00322               repaint();
00323               LastScrollTime=System.currentTimeMillis();
00324        }
00325 
00326        int computeVerticalSize ()
00327        {      if (LineCount==0) return 100;
00328               int h=PageSize*2000/LineCount;
00329               if (h<10) h=10;
00330               return h;
00331        }
00332 
00333        public int setHorizontal (int v)
00334        {      Offset=v/5;
00335               repaint();
00336               return v;
00337        }
00338 
00339        public void save (PrintWriter fo)
00340        {      ListElement e=L.first();
00341               while (e!=null)
00342               {      fo.println(new String(((Line)e.content()).a));
00343                      e=e.next();
00344               }
00345        }
00346 
00347        public TextPosition getposition (int x, int y)
00348        {      if (L.first()==null) return null;
00349               if (y<0) return new TextPosition(TopLine,TopLineCount,0);
00350               if (TopLine==null) return null;
00351               ListElement e=TopLine;
00352               int h=Leading+Height;
00353               if (h==0) return null;
00354               h=y/h;
00355               int i;
00356               for (i=0; i<h; i++)
00357               {      if (e.next()==null || i==PageSize-1)
00358                             return new TextPosition(e,TopLineCount+i,
00359                             ((Line)e.content()).length());
00360                      e=e.next();
00361               }
00362               return new TextPosition(e,TopLineCount+i,
00363                      ((Line)e.content()).getpos(x,2));
00364        }
00365 
00366        public void unmark ()
00367        {      ListElement e=L.first();
00368               while (e!=null)
00369               {      ((Line)e.content()).block(0,Line.NONE);
00370                      e=e.next();
00371               }
00372               repaint();
00373        }
00374 
00375        public void unmark (TextPosition Start, TextPosition End)
00376        {      if (Start==null || End==null) return;
00377               TextPosition P1,P2;
00378               if (Start.before(End)) { P1=Start; P2=End; }
00379               else if (End.before(Start)) { P1=End; P2=Start; }
00380               else return;
00381               ListElement e=P1.L;
00382               while (e!=null && e!=P2.L)
00383               {      ((Line)e.content()).block(0,Line.NONE);
00384                      e=e.next();
00385               }
00386               if (e!=null) ((Line)e.content()).block(0,Line.NONE);
00387               repaint();
00388        }
00389 
00390        public void mark (TextPosition Start, TextPosition End)
00391        {      if (Start==null || End==null) return;
00392               TextPosition P1,P2;
00393               if (Start.before(End)) { P1=Start; P2=End; }
00394               else if (End.before(Start)) { P1=End; P2=Start; }
00395               else return;
00396               ListElement e=P1.L;
00397               ((Line)e.content()).block(P1.LPos,Line.START);
00398               if (e!=P2.L) e=e.next();
00399               while (e!=null && e!=P2.L)
00400               {      ((Line)e.content()).block(0,Line.FULL);
00401                      e=e.next();
00402               }
00403               if (e!=null) ((Line)e.content()).block(P2.LPos,Line.END);
00404               repaint();
00405               requestFocus();
00406        }
00407 
00408        void copy (TextPosition Start, TextPosition End)
00409        {      if (Start==null || End==null) return;
00410               TextPosition P1,P2;
00411               if (Start.before(End)) { P1=Start; P2=End; }
00412               else if (End.before(Start)) { P1=End; P2=Start; }
00413               else return;
00414               String s="";
00415               ListElement e=P1.L;
00416               while (e!=null && e!=P2.L)
00417               {      s=s+((Line)e.content()).getblock()+"\n";
00418                      e=e.next();
00419               }
00420               if (e!=null) s=s+((Line)e.content()).getblock();
00421               new ClipboardCopy(this,this,s);
00422        }
00423 
00424        public void showFirst ()
00425        {      TopLine=L.first();
00426        }
00427 
00428        public void lostOwnership (Clipboard clip, Transferable cont) {}
00429        TextPosition lastpos ()
00430        {      ListElement e=L.last();     
00431               if (e==null) return null;
00432               Line l=(Line)e.content();
00433               return new TextPosition(e,LineCount,l.length());
00434        }
00435 
00436        public void setTabWidth (int t) { TabWidth=t; }
00437        
00438        public boolean hasFocus ()
00439        {      return V.hasFocus();
00440        }
00441        
00442        public void setBackground (Color c)
00443        {      Background=c;
00444               super.setBackground(c);
00445        }
00446        
00447        public void componentHidden (ComponentEvent e) {}
00448        public void componentMoved (ComponentEvent e) {}
00449        public void componentResized (ComponentEvent e)  
00450        {      V.resized();
00451        }
00452        public void componentShown (ComponentEvent e) {}
00453 }