added isabelle jedit -R;
authorwenzelm
Sun Dec 18 21:58:13 2016 +0100 (2016-12-18)
changeset 646028edca3465758
parent 64601 37ce6ceacbb7
child 64603 a7f5e59378f7
added isabelle jedit -R;
errors in session_info/session_content are ignored and deferred to later checks of Build.build;
NEWS
src/Doc/JEdit/JEdit.thy
src/Pure/Tools/build.scala
src/Tools/jEdit/lib/Tools/jedit
src/Tools/jEdit/src/jedit_sessions.scala
src/Tools/jEdit/src/plugin.scala
     1.1 --- a/NEWS	Sun Dec 18 20:01:24 2016 +0100
     1.2 +++ b/NEWS	Sun Dec 18 21:58:13 2016 +0100
     1.3 @@ -6,6 +6,13 @@
     1.4  New in this Isabelle version
     1.5  ----------------------------
     1.6  
     1.7 +*** Prover IDE -- Isabelle/Scala/jEdit ***
     1.8 +
     1.9 +* Command-line invocation "isabelle jedit -R -l LOGIC" opens the ROOT
    1.10 +entry of the specified logic session in the editor, while its parent is
    1.11 +used for formal checking.
    1.12 +
    1.13 +
    1.14  *** HOL ***
    1.15  
    1.16  * Swapped orientation of congruence rules mod_add_left_eq,
    1.17 @@ -31,7 +38,7 @@
    1.18  
    1.19  * The theorem in Permutations has been renamed:
    1.20    bij_swap_ompose_bij ~> bij_swap_compose_bij
    1.21 - 
    1.22 +
    1.23  
    1.24  New in Isabelle2016-1 (December 2016)
    1.25  -------------------------------------
    1.26 @@ -92,6 +99,7 @@
    1.27  * Solve direct: option "solve_direct_strict_warnings" gives explicit
    1.28  warnings for lemma statements with trivial proofs.
    1.29  
    1.30 +
    1.31  *** Prover IDE -- Isabelle/Scala/jEdit ***
    1.32  
    1.33  * More aggressive flushing of machine-generated input, according to
     2.1 --- a/src/Doc/JEdit/JEdit.thy	Sun Dec 18 20:01:24 2016 +0100
     2.2 +++ b/src/Doc/JEdit/JEdit.thy	Sun Dec 18 21:58:13 2016 +0100
     2.3 @@ -233,6 +233,7 @@
     2.4    Options are:
     2.5      -D NAME=X    set JVM system property
     2.6      -J OPTION    add JVM runtime option
     2.7 +    -R           open ROOT entry of logic session and use its parent
     2.8      -b           build only
     2.9      -d DIR       include session directory
    2.10      -f           fresh build
    2.11 @@ -256,6 +257,11 @@
    2.12    The \<^verbatim>\<open>-n\<close> option bypasses the implicit build process for the selected
    2.13    session image.
    2.14  
    2.15 +  Option \<^verbatim>\<open>-R\<close> modifies the meaning of option \<^verbatim>\<open>-l\<close> as follows: the \<^verbatim>\<open>ROOT\<close>
    2.16 +  entry of the specified session is opened in the editor, while its parent
    2.17 +  session is used for formal checking. This facilitates maintenance of a
    2.18 +  broken session, by moving the Prover IDE quickly to relevant source files.
    2.19 +
    2.20    The \<^verbatim>\<open>-m\<close> option specifies additional print modes for the prover process.
    2.21    Note that the system option @{system_option_ref jedit_print_mode} allows to
    2.22    do the same persistently (e.g.\ via the \<^emph>\<open>Plugin Options\<close> dialog of
     3.1 --- a/src/Pure/Tools/build.scala	Sun Dec 18 20:01:24 2016 +0100
     3.2 +++ b/src/Pure/Tools/build.scala	Sun Dec 18 21:58:13 2016 +0100
     3.3 @@ -96,12 +96,12 @@
     3.4    /* source dependencies and static content */
     3.5  
     3.6    sealed case class Session_Content(
     3.7 -    loaded_theories: Set[String],
     3.8 -    known_theories: Map[String, Document.Node.Name],
     3.9 -    keywords: Thy_Header.Keywords,
    3.10 -    syntax: Outer_Syntax,
    3.11 -    sources: List[(Path, SHA1.Digest)],
    3.12 -    session_graph: Graph_Display.Graph)
    3.13 +    loaded_theories: Set[String] = Set.empty,
    3.14 +    known_theories: Map[String, Document.Node.Name] = Map.empty,
    3.15 +    keywords: Thy_Header.Keywords = Nil,
    3.16 +    syntax: Outer_Syntax = Outer_Syntax.empty,
    3.17 +    sources: List[(Path, SHA1.Digest)] = Nil,
    3.18 +    session_graph: Graph_Display.Graph = Graph_Display.empty_graph)
    3.19  
    3.20    sealed case class Deps(deps: Map[String, Session_Content])
    3.21    {
     4.1 --- a/src/Tools/jEdit/lib/Tools/jedit	Sun Dec 18 20:01:24 2016 +0100
     4.2 +++ b/src/Tools/jEdit/lib/Tools/jedit	Sun Dec 18 21:58:13 2016 +0100
     4.3 @@ -98,6 +98,7 @@
     4.4    echo "  Options are:"
     4.5    echo "    -D NAME=X    set JVM system property"
     4.6    echo "    -J OPTION    add JVM runtime option (default $JEDIT_JAVA_SYSTEM_OPTIONS $JEDIT_JAVA_OPTIONS)"
     4.7 +  echo "    -R           open ROOT entry of logic session and use its parent"
     4.8    echo "    -b           build only"
     4.9    echo "    -d DIR       include session directory"
    4.10    echo "    -f           fresh build"
    4.11 @@ -135,6 +136,7 @@
    4.12  BUILD_JARS="jars"
    4.13  ML_PROCESS_POLICY=""
    4.14  JEDIT_SESSION_DIRS=""
    4.15 +JEDIT_LOGIC_ROOT=""
    4.16  JEDIT_LOGIC=""
    4.17  JEDIT_PRINT_MODE=""
    4.18  JEDIT_BUILD_MODE="normal"
    4.19 @@ -142,7 +144,7 @@
    4.20  function getoptions()
    4.21  {
    4.22    OPTIND=1
    4.23 -  while getopts "D:J:bd:fj:l:m:np:s" OPT
    4.24 +  while getopts "D:J:Rbd:fj:l:m:np:s" OPT
    4.25    do
    4.26      case "$OPT" in
    4.27        D)
    4.28 @@ -151,6 +153,9 @@
    4.29        J)
    4.30          JAVA_ARGS["${#JAVA_ARGS[@]}"]="$OPTARG"
    4.31          ;;
    4.32 +      R)
    4.33 +        JEDIT_LOGIC_ROOT="true"
    4.34 +        ;;
    4.35        b)
    4.36          BUILD_ONLY=true
    4.37          ;;
    4.38 @@ -365,7 +370,7 @@
    4.39  
    4.40  if [ "$BUILD_ONLY" = false ]
    4.41  then
    4.42 -  export JEDIT_SESSION_DIRS JEDIT_LOGIC JEDIT_PRINT_MODE JEDIT_BUILD_MODE
    4.43 +  export JEDIT_SESSION_DIRS JEDIT_LOGIC JEDIT_LOGIC_ROOT JEDIT_PRINT_MODE JEDIT_BUILD_MODE
    4.44    export JEDIT_ML_PROCESS_POLICY="$ML_PROCESS_POLICY"
    4.45    classpath "$JEDIT_HOME/dist/jedit.jar"
    4.46    exec isabelle java "${JAVA_ARGS[@]}" isabelle.Main "${ARGS[@]}"
     5.1 --- a/src/Tools/jEdit/src/jedit_sessions.scala	Sun Dec 18 20:01:24 2016 +0100
     5.2 +++ b/src/Tools/jEdit/src/jedit_sessions.scala	Sun Dec 18 21:58:13 2016 +0100
     5.3 @@ -19,10 +19,7 @@
     5.4  
     5.5    private val option_name = "jedit_logic"
     5.6  
     5.7 -  def session_name(): String =
     5.8 -    Isabelle_System.default_logic(
     5.9 -      Isabelle_System.getenv("JEDIT_LOGIC"),
    5.10 -      PIDE.options.string(option_name))
    5.11 +  sealed case class Info(name: String, open_root: Position.T)
    5.12  
    5.13    def session_dirs(): List[Path] = Path.split(Isabelle_System.getenv("JEDIT_SESSION_DIRS"))
    5.14  
    5.15 @@ -32,6 +29,25 @@
    5.16        case s => PIDE.options.value.string("ML_process_policy") = s
    5.17      }
    5.18  
    5.19 +  def session_info(): Info =
    5.20 +  {
    5.21 +    val logic =
    5.22 +      Isabelle_System.default_logic(
    5.23 +        Isabelle_System.getenv("JEDIT_LOGIC"),
    5.24 +        PIDE.options.string(option_name))
    5.25 +
    5.26 +    (for {
    5.27 +      tree <-
    5.28 +        try { Some(Sessions.load(session_options(), dirs = session_dirs())) }
    5.29 +        catch { case ERROR(_) => None }
    5.30 +      info <- tree.lift(logic)
    5.31 +      parent <- info.parent
    5.32 +      if Isabelle_System.getenv("JEDIT_LOGIC_ROOT") == "true"
    5.33 +    } yield Info(parent, info.pos)) getOrElse Info(logic, Position.none)
    5.34 +  }
    5.35 +
    5.36 +  def session_name(): String = session_info().name
    5.37 +
    5.38    def session_build_mode(): String = Isabelle_System.getenv("JEDIT_BUILD_MODE")
    5.39  
    5.40    def session_build(progress: Progress = Ignore_Progress, no_build: Boolean = false): Int =
    5.41 @@ -66,7 +82,10 @@
    5.42    def session_content(inlined_files: Boolean): Build.Session_Content =
    5.43    {
    5.44      val content =
    5.45 -      Build.session_content(PIDE.options.value, inlined_files, session_dirs(), session_name())
    5.46 +      try {
    5.47 +        Build.session_content(PIDE.options.value, inlined_files, session_dirs(), session_name())
    5.48 +      }
    5.49 +      catch { case ERROR(_) => Build.Session_Content() }
    5.50      content.copy(known_theories =
    5.51        content.known_theories.mapValues(name => name.map(File.platform_path(_))))
    5.52    }
     6.1 --- a/src/Tools/jEdit/src/plugin.scala	Sun Dec 18 20:01:24 2016 +0100
     6.2 +++ b/src/Tools/jEdit/src/plugin.scala	Sun Dec 18 21:58:13 2016 +0100
     6.3 @@ -333,9 +333,14 @@
     6.4                "It is for testing only, not for production use.")
     6.5            }
     6.6  
     6.7 -          Session_Build.session_build(jEdit.getActiveView())
     6.8 +          val view = jEdit.getActiveView()
     6.9 +
    6.10 +          Session_Build.session_build(view)
    6.11  
    6.12 -          Keymap_Merge.check_dialog(jEdit.getActiveView())
    6.13 +          Keymap_Merge.check_dialog(view)
    6.14 +
    6.15 +          PIDE.editor.hyperlink_position(true, Document.Snapshot.init,
    6.16 +            JEdit_Sessions.session_info().open_root).foreach(_.follow(view))
    6.17  
    6.18          case msg: BufferUpdate
    6.19          if msg.getWhat == BufferUpdate.LOADED ||