[isabelle-dev] Whole word search

Makarius makarius at sketis.net
Mon Jun 6 21:47:37 CEST 2016

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;
			type = WHITESPACE;
		else if(Character.isLetterOrDigit(ch)
			|| noWordSep.indexOf(ch) != -1)
			type = WORD_CHAR;
			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:

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.


More information about the isabelle-dev mailing list