[isabelle-dev] Whole word search

[Makarius]

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