added jedit option -d;
authorwenzelm
Tue Aug 14 11:37:58 2012 +0200 (2012-08-14)
changeset 487919e8f30bfbdca
parent 48790 6e739225dd8a
child 48792 4aa5b965f70e
added jedit option -d;
doc-src/System/Thy/Interfaces.thy
doc-src/System/Thy/document/Interfaces.tex
src/Pure/System/build.scala
src/Pure/System/session.scala
src/Tools/jEdit/lib/Tools/jedit
src/Tools/jEdit/src/plugin.scala
     1.1 --- a/doc-src/System/Thy/Interfaces.thy	Tue Aug 14 10:44:03 2012 +0200
     1.2 +++ b/doc-src/System/Thy/Interfaces.thy	Tue Aug 14 11:37:58 2012 +0200
     1.3 @@ -15,6 +15,7 @@
     1.4    Options are:
     1.5      -J OPTION    add JVM runtime option (default JEDIT_JAVA_OPTIONS)
     1.6      -b           build only
     1.7 +    -d DIR       include session directory
     1.8      -f           fresh build
     1.9      -j OPTION    add jEdit runtime option (default JEDIT_OPTIONS)
    1.10      -l NAME      logic image name (default ISABELLE_LOGIC)
    1.11 @@ -24,8 +25,12 @@
    1.12  (default Scratch.thy).
    1.13  \end{ttbox}
    1.14  
    1.15 -  The @{verbatim "-l"} option specifies the logic image.  The
    1.16 -  @{verbatim "-m"} option specifies additional print modes.
    1.17 +  The @{verbatim "-l"} option specifies the session name of the logic
    1.18 +  image to be used for proof processing.  Additional session root
    1.19 +  directories may be included via option @{verbatim "-d"} to augment
    1.20 +  that name space (see also \secref{sec:tool-build}).
    1.21 +
    1.22 +  The @{verbatim "-m"} option specifies additional print modes.
    1.23  
    1.24    The @{verbatim "-J"} and @{verbatim "-j"} options allow to pass
    1.25    additional low-level options to the JVM or jEdit, respectively.  The
     2.1 --- a/doc-src/System/Thy/document/Interfaces.tex	Tue Aug 14 10:44:03 2012 +0200
     2.2 +++ b/doc-src/System/Thy/document/Interfaces.tex	Tue Aug 14 11:37:58 2012 +0200
     2.3 @@ -36,6 +36,7 @@
     2.4    Options are:
     2.5      -J OPTION    add JVM runtime option (default JEDIT_JAVA_OPTIONS)
     2.6      -b           build only
     2.7 +    -d DIR       include session directory
     2.8      -f           fresh build
     2.9      -j OPTION    add jEdit runtime option (default JEDIT_OPTIONS)
    2.10      -l NAME      logic image name (default ISABELLE_LOGIC)
    2.11 @@ -45,8 +46,12 @@
    2.12  (default Scratch.thy).
    2.13  \end{ttbox}
    2.14  
    2.15 -  The \verb|-l| option specifies the logic image.  The
    2.16 -  \verb|-m| option specifies additional print modes.
    2.17 +  The \verb|-l| option specifies the session name of the logic
    2.18 +  image to be used for proof processing.  Additional session root
    2.19 +  directories may be included via option \verb|-d| to augment
    2.20 +  that name space (see also \secref{sec:tool-build}).
    2.21 +
    2.22 +  The \verb|-m| option specifies additional print modes.
    2.23  
    2.24    The \verb|-J| and \verb|-j| options allow to pass
    2.25    additional low-level options to the JVM or jEdit, respectively.  The
     3.1 --- a/src/Pure/System/build.scala	Tue Aug 14 10:44:03 2012 +0200
     3.2 +++ b/src/Pure/System/build.scala	Tue Aug 14 11:37:58 2012 +0200
     3.3 @@ -366,13 +366,14 @@
     3.4            deps + (name -> Session_Content(loaded_theories, syntax, sources))
     3.5        }))
     3.6  
     3.7 -  def session_content(session: String): Session_Content =
     3.8 +  def session_content(dirs: List[Path], session: String): Session_Content =
     3.9    {
    3.10 -    val (_, tree) = find_sessions(Options.init(), Nil).required(false, Nil, List(session))
    3.11 +    val (_, tree) =
    3.12 +      find_sessions(Options.init(), dirs.map((false, _))).required(false, Nil, List(session))
    3.13      dependencies(false, tree)(session)
    3.14    }
    3.15  
    3.16 -  def outer_syntax(session: String): Outer_Syntax = session_content(session).syntax
    3.17 +  def outer_syntax(session: String): Outer_Syntax = session_content(Nil, session).syntax
    3.18  
    3.19  
    3.20    /* jobs */
     4.1 --- a/src/Pure/System/session.scala	Tue Aug 14 10:44:03 2012 +0200
     4.2 +++ b/src/Pure/System/session.scala	Tue Aug 14 11:37:58 2012 +0200
     4.3 @@ -171,7 +171,7 @@
     4.4  
     4.5    /* actor messages */
     4.6  
     4.7 -  private case class Start(logic: String, args: List[String])
     4.8 +  private case class Start(dirs: List[Path], logic: String, args: List[String])
     4.9    private case object Cancel_Execution
    4.10    private case class Edit(edits: List[Document.Edit_Text])
    4.11    private case class Change(
    4.12 @@ -377,12 +377,12 @@
    4.13        receiveWithin(delay_commands_changed.flush_timeout) {
    4.14          case TIMEOUT => delay_commands_changed.flush()
    4.15  
    4.16 -        case Start(name, args) if prover.isEmpty =>
    4.17 +        case Start(dirs, name, args) if prover.isEmpty =>
    4.18            if (phase == Session.Inactive || phase == Session.Failed) {
    4.19              phase = Session.Startup
    4.20  
    4.21              // FIXME static init in main constructor
    4.22 -            val content = Build.session_content(name)
    4.23 +            val content = Build.session_content(dirs, name)
    4.24              thy_load.register_thys(content.loaded_theories)
    4.25              base_syntax = content.syntax
    4.26  
    4.27 @@ -440,7 +440,8 @@
    4.28  
    4.29    /* actions */
    4.30  
    4.31 -  def start(name: String, args: List[String]) { session_actor ! Start(name, args) }
    4.32 +  def start(dirs: List[Path], name: String, args: List[String])
    4.33 +  { session_actor ! Start(dirs, name, args) }
    4.34  
    4.35    def stop() { commands_changed_buffer !? Stop; change_parser !? Stop; session_actor !? Stop }
    4.36  
     5.1 --- a/src/Tools/jEdit/lib/Tools/jedit	Tue Aug 14 10:44:03 2012 +0200
     5.2 +++ b/src/Tools/jEdit/lib/Tools/jedit	Tue Aug 14 11:37:58 2012 +0200
     5.3 @@ -52,6 +52,7 @@
     5.4    echo "    -J OPTION    add JVM runtime option"
     5.5    echo "                 (default JEDIT_JAVA_OPTIONS=$JEDIT_JAVA_OPTIONS)"
     5.6    echo "    -b           build only"
     5.7 +  echo "    -d DIR       include session directory"
     5.8    echo "    -f           fresh build"
     5.9    echo "    -j OPTION    add jEdit runtime option"
    5.10    echo "                 (default JEDIT_OPTIONS=$JEDIT_OPTIONS)"
    5.11 @@ -82,13 +83,14 @@
    5.12  
    5.13  BUILD_ONLY=false
    5.14  BUILD_JARS="jars"
    5.15 +JEDIT_SESSION_DIRS=""
    5.16  JEDIT_LOGIC="$ISABELLE_LOGIC"
    5.17  JEDIT_PRINT_MODE=""
    5.18  
    5.19  function getoptions()
    5.20  {
    5.21    OPTIND=1
    5.22 -  while getopts "J:bdfj:l:m:" OPT
    5.23 +  while getopts "J:bd:fj:l:m:" OPT
    5.24    do
    5.25      case "$OPT" in
    5.26        J)
    5.27 @@ -97,6 +99,13 @@
    5.28        b)
    5.29          BUILD_ONLY=true
    5.30          ;;
    5.31 +      d)
    5.32 +        if [ -z "$JEDIT_SESSION_DIRS" ]; then
    5.33 +          JEDIT_SESSION_DIRS="$OPTARG"
    5.34 +        else
    5.35 +          JEDIT_SESSION_DIRS="$JEDIT_SESSION_DIRS:$OPTARG"
    5.36 +        fi
    5.37 +        ;;
    5.38        f)
    5.39          BUILD_JARS="jars_fresh"
    5.40          ;;
    5.41 @@ -283,7 +292,7 @@
    5.42        ;;
    5.43    esac
    5.44  
    5.45 -  export JEDIT_LOGIC JEDIT_PRINT_MODE
    5.46 +  export JEDIT_SESSION_DIRS JEDIT_LOGIC JEDIT_PRINT_MODE
    5.47  
    5.48    exec "$ISABELLE_TOOL" java "${JAVA_ARGS[@]}" \
    5.49      -jar "$(jvmpath "$JEDIT_HOME/dist/jedit.jar")" \
     6.1 --- a/src/Tools/jEdit/src/plugin.scala	Tue Aug 14 10:44:03 2012 +0200
     6.2 +++ b/src/Tools/jEdit/src/plugin.scala	Tue Aug 14 11:37:58 2012 +0200
     6.3 @@ -300,6 +300,7 @@
     6.4  
     6.5    def start_session()
     6.6    {
     6.7 +    val dirs = Path.split(Isabelle_System.getenv("JEDIT_SESSION_DIRS"))
     6.8      val modes = space_explode(',', Isabelle_System.getenv("JEDIT_PRINT_MODE")).map("-m" + _)
     6.9      val logic = {
    6.10        val logic = Property("logic")
    6.11 @@ -307,7 +308,7 @@
    6.12        else Isabelle.default_logic()
    6.13      }
    6.14      val name = Path.explode(logic).base.implode  // FIXME more robust session name
    6.15 -    session.start(name, modes ::: List(logic))
    6.16 +    session.start(dirs, name, modes ::: List(logic))
    6.17    }
    6.18  
    6.19