src/Doc/JEdit/JEdit.thy
changeset 66574 e16b27bd3f76
parent 66462 0a8277e9cfd6
child 66681 0879f2045965
     1.1 --- a/src/Doc/JEdit/JEdit.thy	Thu Aug 31 17:21:38 2017 +0200
     1.2 +++ b/src/Doc/JEdit/JEdit.thy	Thu Aug 31 17:31:56 2017 +0200
     1.3 @@ -232,7 +232,7 @@
     1.4    Options are:
     1.5      -D NAME=X    set JVM system property
     1.6      -J OPTION    add JVM runtime option
     1.7 -    -R           restrict to parent of logic session and open its ROOT
     1.8 +    -R           open ROOT entry of logic session and use its parent
     1.9      -b           build only
    1.10      -d DIR       include session directory
    1.11      -f           fresh build
    1.12 @@ -256,12 +256,10 @@
    1.13    The \<^verbatim>\<open>-n\<close> option bypasses the implicit build process for the selected
    1.14    session image.
    1.15  
    1.16 -  Option \<^verbatim>\<open>-R\<close> modifies the meaning of option \<^verbatim>\<open>-l\<close>~\<open>session\<close> as follows: the
    1.17 -  parent image of the \<open>session\<close> is used, with qualified theory imports
    1.18 -  restricted to that portion of the session graph. Moreover, the \<^verbatim>\<open>ROOT\<close> entry
    1.19 -  of the \<open>session\<close> is opened in the editor. This facilitates maintenance of a
    1.20 -  particular session, by moving the Prover IDE quickly to relevant source
    1.21 -  files.
    1.22 +  Option \<^verbatim>\<open>-R\<close> modifies the meaning of option \<^verbatim>\<open>-l\<close> as follows: the \<^verbatim>\<open>ROOT\<close>
    1.23 +  entry of the specified session is opened in the editor, while its parent
    1.24 +  session is used for formal checking. This facilitates maintenance of a
    1.25 +  broken session, by moving the Prover IDE quickly to relevant source files.
    1.26  
    1.27    The \<^verbatim>\<open>-m\<close> option specifies additional print modes for the prover process.
    1.28    Note that the system option @{system_option_ref jedit_print_mode} allows to