factor/jedit/FactorPlugin.java

   1 /* :folding=explicit:collapseFolds=1: */
   2
   3 /*
   4  * $Id$
   5  *
   6  * Copyright (C) 2004 Slava Pestov.
   7  *
   8  * Redistribution and use in source and binary forms, with or without
   9  * modification, are permitted provided that the following conditions are met:
  10  *
  11  * 1. Redistributions of source code must retain the above copyright notice,
  12  *    this list of conditions and the following disclaimer.
  13  *
  14  * 2. Redistributions in binary form must reproduce the above copyright notice,
  15  *    this list of conditions and the following disclaimer in the documentation
  16  *    and/or other materials provided with the distribution.
  17  *
  18  * THIS SOFTWARE IS PROVIDED ``AS IS'' AND ANY EXPRESS OR IMPLIED WARRANTIES,
  19  * INCLUDING, BUT NOT LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND
  20  * FITNESS FOR A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE
  21  * DEVELOPERS AND CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL,
  22  * SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO,
  23  * PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS;
  24  * OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY,
  25  * WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR
  26  * OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF
  27  * ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
  28  */
  29
  30 package factor.jedit;
  31
  32 import factor.*;
  33 import java.io.*;
  34 import java.util.*;
  35 import org.gjt.sp.jedit.gui.*;
  36 import org.gjt.sp.jedit.textarea.*;
  37 import org.gjt.sp.jedit.*;
  38 import org.gjt.sp.util.Log;
  39 import console.*;
  40 import sidekick.*;
  41
  42 public class FactorPlugin extends EditPlugin
  43 {
  44         private static ExternalFactor external;
  45         private static Process process;
  46         private static int PORT = 9999;
  47
  48         //{{{ getPluginPath() method
  49         private String getPluginPath()
  50         {
  51                 return MiscUtilities.getParentOfPath(
  52                         jEdit.getPlugin("factor.jedit.FactorPlugin")
  53                         .getPluginJAR().getPath())
  54                         + "Factor";
  55         } //}}}
  56
  57         //{{{ start() method
  58         public void start()
  59         {
  60                 BeanShell.eval(null,BeanShell.getNameSpace(),
  61                         "import factor.*;\nimport factor.jedit.*;\n");
  62                 String program = jEdit.getProperty("factor.external.program");
  63                 String image = jEdit.getProperty("factor.external.image");
  64                 if(program == null || image == null
  65                         || program.length() == 0 || image.length() == 0)
  66                 {
  67                         jEdit.setProperty("factor.external.program",
  68                                 MiscUtilities.constructPath(getPluginPath(),"f"));
  69                         jEdit.setProperty("factor.external.image",
  70                                 MiscUtilities.constructPath(getPluginPath(),"factor.image"));
  71                 }
  72         } //}}}
  73
  74         //{{{ stop() method
  75         public void stop()
  76         {
  77                 stopExternalInstance();
  78
  79                 Buffer buffer = jEdit.getFirstBuffer();
  80                 while(buffer != null)
  81                 {
  82                         buffer.setProperty(FactorSideKickParser.WORDS_PROPERTY,null);
  83                         buffer = buffer.getNext();
  84                 }
  85         } //}}}
  86
  87         //{{{ addNonEmpty() method
  88         private static void addNonEmpty(String[] input, List output)
  89         {
  90                 for(int i = 0; i < input.length; i++)
  91                 {
  92                         if(input[i].length() != 0)
  93                                 output.add(input[i]);
  94                 }
  95         } //}}}
  96
  97         //{{{ getExternalInstance() method
  98         /**
  99          * Returns the object representing a connection to an external Factor instance.
 100          * It will start the interpreter if it's not already running.
 101          */
 102         public synchronized static ExternalFactor getExternalInstance()
 103         {
 104                 if(external == null)
 105                 {
 106                         InputStream in = null;
 107                         OutputStream out = null;
 108
 109                         try
 110                         {
 111                                 String exePath = jEdit.getProperty(
 112                                         "factor.external.program");
 113                                 String imagePath = jEdit.getProperty(
 114                                         "factor.external.image");
 115                                 List args = new ArrayList();
 116                                 args.add(exePath);
 117                                 args.add(imagePath);
 118                                 args.add("-shell=telnet");
 119                                 args.add("-telnetd-port=" + PORT);
 120                                 String[] extraArgs = jEdit.getProperty(
 121                                         "factor.external.args")
 122                                         .split(" ");
 123                                 addNonEmpty(extraArgs,args);
 124                                 process = Runtime.getRuntime().exec(
 125                                         (String[])args.toArray(
 126                                         new String[args.size()]),
 127                                         null,
 128                                         new File(MiscUtilities
 129                                         .getParentOfPath(imagePath)));
 130
 131                                 external = new ExternalFactor(PORT);
 132                         }
 133                         catch(Exception e)
 134                         {
 135                                 Log.log(Log.ERROR,FactorPlugin.class,
 136                                         "Cannot start external Factor:");
 137                                 Log.log(Log.ERROR,FactorPlugin.class,e);
 138                                 process = null;
 139                         }
 140                 }
 141
 142                 return external;
 143         } //}}}
 144
 145         //{{{ getFactorShell() method
 146         public static FactorShell getFactorShell()
 147         {
 148                 return ((FactorShell)ServiceManager.getService("console.Shell","Factor"));
 149         } //}}}
 150
 151         //{{{ stopExternalInstance() method
 152         /**
 153          * Stops the external interpreter.
 154          */
 155         public static void stopExternalInstance()
 156         {
 157                 getFactorShell().closeStreams();
 158
 159                 if(external != null)
 160                 {
 161                         external.close();
 162                         try
 163                         {
 164                                 process.getErrorStream().close();
 165                                 process.getInputStream().close();
 166                                 process.getOutputStream().close();
 167                                 process.waitFor();
 168                         }
 169                         catch(Exception e)
 170                         {
 171                                 Log.log(Log.DEBUG,FactorPlugin.class,e);
 172                         }
 173                         external = null;
 174                         process = null;
 175                 }
 176         } //}}}
 177
 178         //{{{ restartExternalInstance() method
 179         /**
 180          * Restart the external interpreter.
 181          */
 182         public static void restartExternalInstance()
 183         {
 184                 stopExternalInstance();
 185                 getExternalInstance();
 186                 FactorPlugin.getFactorShell().openStreams();
 187         } //}}}
 188
 189         //{{{ getSideKickParser() method
 190         public static FactorSideKickParser getSideKickParser()
 191         {
 192                 return (FactorSideKickParser)ServiceManager.getService(
 193                         "sidekick.SideKickParser","factor");
 194         } //}}}
 195
 196         //{{{ evalInListener() method
 197         public static void evalInListener(View view, String cmd)
 198         {
 199                 DockableWindowManager wm = view.getDockableWindowManager();
 200                 wm.addDockableWindow("console");
 201                 Console console = (Console)wm.getDockableWindow("console");
 202                 console.run(Shell.getShell("Factor"),console,cmd);
 203         } //}}}
 204
 205         //{{{ evalInWire() method
 206         public static String evalInWire(String cmd) throws IOException
 207         {
 208                 return getExternalInstance().eval(cmd);
 209         } //}}}
 210
 211         //{{{ lookupWord() method
 212         /**
 213          * Look up the given Factor word in the vocabularies USE:d in the given view.
 214          */
 215         public static FactorWord lookupWord(View view, String word)
 216         {
 217                 SideKickParsedData data = SideKickParsedData.getParsedData(view);
 218                 if(data instanceof FactorParsedData)
 219                 {
 220                         FactorParsedData fdata = (FactorParsedData)data;
 221                         return getExternalInstance().searchVocabulary(fdata.use,word);
 222                 }
 223                 else
 224                         return null;
 225         } //}}}
 226
 227         //{{{ factorWord() method
 228         /**
 229          * Look up the given Factor word in the vocabularies USE:d in the given view.
 230          */
 231         public static String factorWord(View view, String word)
 232         {
 233                 SideKickParsedData data = SideKickParsedData
 234                         .getParsedData(view);
 235                 if(data instanceof FactorParsedData)
 236                 {
 237                         FactorParsedData fdata = (FactorParsedData)data;
 238                         return "\""
 239                                 + FactorReader.charsToEscapes(word)
 240                                 + "\" " + FactorReader.unparseObject(fdata.use)
 241                                 + " search";
 242                 }
 243                 else
 244                         return null;
 245         } //}}}
 246
 247         //{{{ factorWord() method
 248         /**
 249          * Build a Factor expression for pushing the selected word on the stack
 250          */
 251         public static String factorWord(View view)
 252         {
 253                 JEditTextArea textArea = view.getTextArea();
 254                 String word = FactorPlugin.getWordAtCaret(textArea);
 255                 if(word == null)
 256                         return null;
 257                 else
 258                         return factorWord(view,word);
 259         } //}}}
 260
 261         //{{{ factorWord() method
 262         /**
 263          * Build a Factor expression for pushing the selected word on the stack
 264          */
 265         public static String factorWord(FactorWord word)
 266         {
 267                 return FactorReader.unparseObject(word.name)
 268                         + " [ " + FactorReader.unparseObject(word.vocabulary)
 269                         + " ] search";
 270         } //}}}
 271
 272         //{{{ factorWordOutputOp() method
 273         /**
 274          * Apply a Factor word to the selected word.
 275          */
 276         public static void factorWordOutputOp(View view, String op)
 277         {
 278                 String word = factorWord(view);
 279                 if(word == null)
 280                         view.getToolkit().beep();
 281                 else
 282                         evalInListener(view,word + " " + op);
 283         } //}}}
 284
 285         //{{{ factorWordWireOp() method
 286         /**
 287          * Apply a Factor word to the selected word.
 288          */
 289         public static void factorWordWireOp(View view, String op) throws IOException
 290         {
 291                 String word = factorWord(view);
 292                 if(word == null)
 293                         view.getToolkit().beep();
 294                 else
 295                         evalInWire(word + " " + op);
 296         } //}}}
 297
 298         //{{{ toWordArray() method
 299         public static FactorWord[] toWordArray(Set completions)
 300         {
 301                 FactorWord[] w = (FactorWord[])completions.toArray(new FactorWord[
 302                         completions.size()]);
 303                 Arrays.sort(w,new MiscUtilities.StringICaseCompare());
 304
 305                 return w;
 306         } //}}}
 307
 308         //{{{ getCompletions() method
 309         /**
 310          * Returns all words in all vocabularies.
 311          *
 312          * @param anywhere If true, matches anywhere in the word name are
 313          * returned; otherwise, only matches from beginning.
 314          */
 315         public static Set getCompletions(String word, boolean anywhere)
 316         {
 317                 try
 318                 {
 319                         Set completions = new HashSet();
 320                         getExternalInstance().getCompletions(
 321                                 getExternalInstance().getVocabularies(),
 322                                 word,
 323                                 anywhere,
 324                                 completions);
 325                         return completions;
 326                 }
 327                 catch(Exception e)
 328                 {
 329                         throw new RuntimeException(e);
 330                 }
 331         } //}}}
 332
 333         //{{{ getWordStartIndex() method
 334         public static int getWordStartOffset(String line, int caret)
 335         {
 336                 ReadTable readtable = ReadTable.DEFAULT_READTABLE;
 337
 338                 int start = caret;
 339                 while(start > 0)
 340                 {
 341                         if(readtable.getCharacterType(line.charAt(start - 1))
 342                                 == ReadTable.WHITESPACE)
 343                         {
 344                                 break;
 345                         }
 346                         else
 347                                 start--;
 348                 }
 349
 350                 return start;
 351         } //}}}
 352
 353         //{{{ getWordAtCaret() method
 354         public static String getWordAtCaret(JEditTextArea textArea)
 355         {
 356                 if(textArea.getSelectionCount() != 0)
 357                         return textArea.getSelectedText();
 358
 359                 String line = textArea.getLineText(textArea.getCaretLine());
 360                 if(line.length() == 0)
 361                         return null;
 362
 363                 int caret = textArea.getCaretPosition()
 364                         - textArea.getLineStartOffset(
 365                         textArea.getCaretLine());
 366                 if(caret == line.length())
 367                         caret--;
 368
 369                 ReadTable readtable = ReadTable.DEFAULT_READTABLE;
 370
 371                 if(readtable.getCharacterType(line.charAt(caret))
 372                         == ReadTable.WHITESPACE)
 373                 {
 374                         return null;
 375                 }
 376
 377                 int start = getWordStartOffset(line,caret);
 378
 379                 int end = caret;
 380                 do
 381                 {
 382                         if(readtable.getCharacterType(line.charAt(end))
 383                                 == ReadTable.WHITESPACE)
 384                         {
 385                                 break;
 386                         }
 387                         else
 388                                 end++;
 389                 }
 390                 while(end < line.length());
 391
 392                 return line.substring(start,end);
 393         } //}}}
 394
 395         //{{{ showStatus() method
 396         public static void showStatus(View view, String msg, String arg)
 397         {
 398                 view.getStatus().setMessage(
 399                         jEdit.getProperty("factor.status." + msg,
 400                         new String[] { arg }));
 401         } //}}}
 402
 403         //{{{ isUsed() method
 404         public static boolean isUsed(View view, String vocab)
 405         {
 406                 SideKickParsedData data = SideKickParsedData
 407                         .getParsedData(view);
 408                 if(data instanceof FactorParsedData)
 409                 {
 410                         FactorParsedData fdata = (FactorParsedData)data;
 411                         Cons use = fdata.use;
 412                         return Cons.contains(use,vocab);
 413                 }
 414                 else
 415                         return false;
 416         } //}}}
 417
 418         //{{{ findAllWordsNamed() method
 419         private static FactorWord[] findAllWordsNamed(View view, String word)
 420                 throws Exception
 421         {
 422                 ExternalFactor external = getExternalInstance();
 423
 424                 ArrayList words = new ArrayList();
 425
 426                 Cons vocabs = external.getVocabularies();
 427                 while(vocabs != null)
 428                 {
 429                         String vocab = (String)vocabs.car;
 430                         FactorWord w = (FactorWord)external.searchVocabulary(
 431                                 new Cons(vocab,null),word);
 432                         if(w != null)
 433                                 words.add(w);
 434                         vocabs = vocabs.next();
 435                 }
 436                 return (FactorWord[])words.toArray(new FactorWord[words.size()]);
 437         } //}}}
 438
 439         //{{{ insertUseDialog() method
 440         public static void insertUseDialog(View view, String word)
 441         {
 442                 try
 443                 {
 444                         FactorWord[] words = findAllWordsNamed(view,word);
 445                         if(words.length == 0)
 446                                 view.getToolkit().beep();
 447                         else if(words.length == 1)
 448                                 insertUse(view,words[0].vocabulary);
 449                         else
 450                                 new InsertUseDialog(view,getSideKickParser(),words);
 451                 }
 452                 catch(Exception e)
 453                 {
 454                         throw new RuntimeException(e);
 455                 }
 456         } //}}}
 457
 458         //{{{ insertUse() method
 459         public static void insertUse(View view, String vocab)
 460         {
 461                 if(isUsed(view,vocab))
 462                 {
 463                         showStatus(view,"already-used",vocab);
 464                         return;
 465                 }
 466
 467                 Buffer buffer = view.getBuffer();
 468                 int lastUseOffset = 0;
 469                 boolean leadingNewline = false;
 470                 boolean seenUse = false;
 471
 472                 for(int i = 0; i < buffer.getLineCount(); i++)
 473                 {
 474                         String text = buffer.getLineText(i).trim();
 475                         if(text.startsWith("IN:") || text.startsWith("USE:"))
 476                         {
 477                                 lastUseOffset = buffer.getLineEndOffset(i) - 1;
 478                                 leadingNewline = true;
 479                                 seenUse = true;
 480                         }
 481                         else if(text.startsWith("!") && !seenUse)
 482                         {
 483                                 lastUseOffset = buffer.getLineEndOffset(i) - 1;
 484                                 leadingNewline = true;
 485                         }
 486                         else if(text.length() == 0 && !seenUse)
 487                         {
 488                                 if(i == 0)
 489                                         lastUseOffset = 0;
 490                                 else
 491                                         lastUseOffset  = buffer.getLineEndOffset(i - 1) - 1;
 492                         }
 493                         else
 494                         {
 495                                 break;
 496                         }
 497                 }
 498
 499                 String decl = "USE: " + vocab;
 500                 if(leadingNewline)
 501                         decl = "\n" + decl;
 502                 if(lastUseOffset == 0)
 503                         decl = decl + "\n";
 504                 buffer.insert(lastUseOffset,decl);
 505                 showStatus(view,"inserted-use",decl);
 506         } //}}}
 507
 508         //{{{ extractWord() method
 509         public static void extractWord(View view)
 510         {
 511                 JEditTextArea textArea = view.getTextArea();
 512                 Buffer buffer = textArea.getBuffer();
 513                 String selection = textArea.getSelectedText();
 514                 if(selection == null)
 515                         selection = "";
 516
 517                 SideKickParsedData data = SideKickParsedData
 518                         .getParsedData(view);
 519                 if(!(data instanceof FactorParsedData))
 520                 {
 521                         view.getToolkit().beep();
 522                         return;
 523                 }
 524
 525                 Asset asset = data.getAssetAtPosition(
 526                         textArea.getCaretPosition());
 527
 528                 if(asset == null)
 529                 {
 530                         GUIUtilities.error(view,"factor.extract-word-where",null);
 531                         return;
 532                 }
 533
 534                 String newWord = GUIUtilities.input(view,
 535                         "factor.extract-word",null);
 536                 if(newWord == null)
 537                         return;
 538
 539                 int start = asset.start.getOffset();
 540                 /* Hack */
 541                 start = buffer.getLineStartOffset(
 542                         buffer.getLineOfOffset(start));
 543
 544                 String indent = MiscUtilities.createWhiteSpace(
 545                         buffer.getIndentSize(),
 546                         (buffer.getBooleanProperty("noTabs") ? 0
 547                         : buffer.getTabSize()));
 548
 549                 String newDef = ": " + newWord + "\n" + indent
 550                         + selection.trim() + " ;\n\n" ;
 551
 552                 try
 553                 {
 554                         buffer.beginCompoundEdit();
 555
 556                         buffer.insert(start,newDef);
 557                         textArea.setSelectedText(newWord);
 558                 }
 559                 finally
 560                 {
 561                         buffer.endCompoundEdit();
 562                 }
 563         } //}}}
 564 }