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

Reply via email to