On 06/06/16 21:29, Makarius wrote: > It means that the parts of long identifiers can be selected individually > (e.g. via double-clicked). It also has an effect on searching "x" in > "x.", but note that the lambda in "λx." is still a word character. > (Maybe that should be changed as well.)
Now that is really hardwired in jEdit/org/gjt/sp/jedit/TextUtilities.java: //{{{ getCharType() method /** * Returns the type of the char. * * @param ch the character * @param noWordSep Characters that are non-alphanumeric, but * should be treated as word characters anyway, it must not be null * @return the type of the char : {@link #WHITESPACE}, * {@link #WORD_CHAR}, {@link #SYMBOL} * @since jEdit 4.4pre1 */ public static int getCharType(char ch, String noWordSep) { int type; if(Character.isWhitespace(ch)) type = WHITESPACE; else if(Character.isLetterOrDigit(ch) || noWordSep.indexOf(ch) != -1) type = WORD_CHAR; else type = SYMBOL; return type; } //}}} Character.isLetterOrDigit actually only works for old 16bit Unicode, so one could in principle evade to a proper mathematical lambda from higher ranges, see also this rejected idea for GHC unicode syntax: https://ghc.haskell.org/trac/ghc/ticket/1102 This would stretch an accidental situation in the jEdit code-base a bit far, and we don't really need it anymore due to isabelle.select-entity. Makarius _______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev