products/Sources/formale Sprachen/Isabelle/Tools/jEdit/dist/macros/Interface/  image not shown  

Quellcode-Bibliothek

© Kompilation durch diese Firma

[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]

Datei:   Sprache: Unknown

Haftungsausschluß.bsh KontaktLex {Lex[95] C[116] Abap[137]}diese Dinge liegen außhalb unserer Verantwortung

/*
* Increase_Font_Size.bsh - a BeanShell macro for the jEdit text
* editor - Increases editor & gutter font size by 1.
*
* Copyright (C) 2003 Ollie Rutherfurd <[email protected]>
*
* $Id: Increase_Font_Size.bsh 21353 2012-03-14 09:46:51Z jojaba_67 $
*/

//Localization
final static String FontSizeMessage = jEdit.getProperty("macro.rs.ChangeFontSize.FontSize.message", "Font size now:");
 
//Process
increaseFontSize()
{
 FONT_SIZE = "view.fontsize";
 GUTTER_FONT_SIZE = "view.gutter.fontsize";
 CONSOLE_FONT_SIZE = "console.fontsize";
 size = jEdit.getIntegerProperty(FONT_SIZE,12) + 1;
 jEdit.setIntegerProperty(FONT_SIZE,size);
 jEdit.setIntegerProperty(GUTTER_FONT_SIZE,size);
 jEdit.setIntegerProperty(CONSOLE_FONT_SIZE,size);
 jEdit.propertiesChanged();
 jEdit.saveSettings();
 view.getStatus().setMessageAndClear(FontSizeMessage + " " + size);
}

increaseFontSize();

/*

 Macro index data (in DocBook format)

<listitem>
 <para><filename>Increase_Font_Size.bsh</filename></para>
 <abstract><para>
  Increases the font size in the gutter and text area by 1 point.
 </para></abstract>
</listitem>

*/

[ Seitenstruktur0.78Drucken  ]