src/Tools/jEdit/src/jedit/plugin.scala
changeset 39517 e036c67448e6
parent 39515 57ceabb0bb8e
child 39518 96180281c3b2
     1.1 --- a/src/Tools/jEdit/src/jedit/plugin.scala	Sat Sep 18 15:50:29 2010 +0200
     1.2 +++ b/src/Tools/jEdit/src/jedit/plugin.scala	Sat Sep 18 16:05:12 2010 +0200
     1.3 @@ -14,6 +14,7 @@
     1.4  import javax.swing.JTextArea
     1.5  
     1.6  import scala.collection.mutable
     1.7 +import scala.swing.ComboBox
     1.8  
     1.9  import org.gjt.sp.jedit.{jEdit, GUIUtilities, EBMessage, EBPlugin,
    1.10    Buffer, EditPane, ServiceManager, View}
    1.11 @@ -120,27 +121,6 @@
    1.12    }
    1.13  
    1.14  
    1.15 -  /* settings */
    1.16 -
    1.17 -  def default_logic(): String =
    1.18 -  {
    1.19 -    val logic = system.getenv("JEDIT_LOGIC")
    1.20 -    if (logic != "") logic
    1.21 -    else system.getenv_strict("ISABELLE_LOGIC")
    1.22 -  }
    1.23 -
    1.24 -  def isabelle_args(): List[String] =
    1.25 -  {
    1.26 -    val modes = system.getenv("JEDIT_PRINT_MODE").split(",").toList.map("-m" + _)
    1.27 -    val logic = {
    1.28 -      val logic = Property("logic")
    1.29 -      if (logic != null && logic != "") logic
    1.30 -      else default_logic()
    1.31 -    }
    1.32 -    modes ++ List(logic)
    1.33 -  }
    1.34 -
    1.35 -
    1.36    /* main jEdit components */
    1.37  
    1.38    def jedit_buffers(): Iterator[Buffer] = jEdit.getBuffers().iterator
    1.39 @@ -195,6 +175,45 @@
    1.40      }
    1.41  
    1.42  
    1.43 +  /* logic image */
    1.44 +
    1.45 +  def default_logic(): String =
    1.46 +  {
    1.47 +    val logic = system.getenv("JEDIT_LOGIC")
    1.48 +    if (logic != "") logic
    1.49 +    else system.getenv_strict("ISABELLE_LOGIC")
    1.50 +  }
    1.51 +
    1.52 +  class Logic_Entry(val name: String, val description: String)
    1.53 +  {
    1.54 +    override def toString = description
    1.55 +  }
    1.56 +
    1.57 +  def logic_selector(logic: String): ComboBox[Logic_Entry] =
    1.58 +  {
    1.59 +    val entries =
    1.60 +      new Logic_Entry("", "default (" + default_logic() + ")") ::
    1.61 +        system.find_logics().map(name => new Logic_Entry(name, name))
    1.62 +    val component = new ComboBox(entries)
    1.63 +    entries.find(_.name == logic) match {
    1.64 +      case None =>
    1.65 +      case Some(entry) => component.selection.item = entry
    1.66 +    }
    1.67 +    component
    1.68 +  }
    1.69 +
    1.70 +  def isabelle_args(): List[String] =
    1.71 +  {
    1.72 +    val modes = system.getenv("JEDIT_PRINT_MODE").split(",").toList.map("-m" + _)
    1.73 +    val logic = {
    1.74 +      val logic = Property("logic")
    1.75 +      if (logic != null && logic != "") logic
    1.76 +      else default_logic()
    1.77 +    }
    1.78 +    modes ++ List(logic)
    1.79 +  }
    1.80 +
    1.81 +
    1.82    /* manage prover */  // FIXME async!?
    1.83  
    1.84    private def prover_started(view: View): Boolean =