diff --git a/Admin/lib/Tools/makedist b/Admin/lib/Tools/makedist
--- a/Admin/lib/Tools/makedist
+++ b/Admin/lib/Tools/makedist
@@ -1,219 +1,233 @@
 #!/usr/bin/env bash
 #
 # Author: Makarius
 #
 # DESCRIPTION: make Isabelle distribution from repository
 
 ## global parameters
 
 umask 022
 
 HG="${HG:-hg}"
 
 DISTPREFIX="${DISTPREFIX:-$HOME/tmp/isadist}"
 
 
 ## diagnostics
 
 PRG="$(basename "$0")"
 
 function usage()
 {
   echo
   echo "Usage: isabelle $PRG [OPTIONS] [VERSION]"
   echo
   echo "  Options are:"
+  echo "    -O           official release (not release-candidate)"
   echo "    -d DIR       global directory prefix (default: \"$DISTPREFIX\")"
   echo "    -j INT       maximum number of parallel jobs (default 1)"
   echo "    -r RELEASE   proper release with name"
   echo
   echo "  Make Isabelle distribution from the local repository clone."
   echo
   echo "  VERSION identifies the snapshot, using usual Mercurial terminology;"
   echo "  the default is RELEASE if given, otherwise \"tip\"."
   echo
   echo "  Add-on components are that of the running Isabelle version!"
   echo
   exit 1
 }
 
 function fail()
 {
   echo "$1" >&2
   exit 2
 }
 
 function check_number()
 {
   [ -n "$1" -a -z "$(echo "$1" | tr -d '[0-9]')" ] || fail "Bad number: \"$1\""
 }
 
 
 ## process command line
 
 # options
 
+OFFICIAL_RELEASE="false"
 JOBS=""
 RELEASE=""
 
 while getopts "d:j:r:" OPT
 do
   case "$OPT" in
+    O)
+      OFFICIAL_RELEASE="true"
+      ;;
     d)
       DISTPREFIX="$OPTARG"
       ;;
     j)
       check_number "$OPTARG"
       JOBS="-j $OPTARG"
       ;;
     r)
       RELEASE="$OPTARG"
       ;;
     \?)
       usage
       ;;
   esac
 done
 
 shift $(($OPTIND - 1))
 
 
 # args
 
 VERSION=""
 [ "$#" -gt 0 ] && { VERSION="$1"; shift; }
 [ -z "$VERSION" ] && VERSION="$RELEASE"
 [ -z "$VERSION" ] && VERSION="tip"
 
 [ "$#" -gt 0 ] && usage
 
 IDENT=$("$HG" --repository "$ISABELLE_HOME" id -r "$VERSION" -i)
 [ -z "$IDENT" ] && fail "Bad repository version: \"$VERSION\""
 
 
 ## main
 
 # dist name
 
 DATE=$(env LC_ALL=C date "+%d-%b-%Y")
 DISTDATE=$(env LC_ALL=C date "+%B %Y")
 
 if [ -z "$RELEASE" ]; then
   DISTNAME="Isabelle_$DATE"
   DISTVERSION="Isabelle repository snapshot $IDENT $DATE"
 else
   DISTNAME="$RELEASE"
   DISTVERSION="$DISTNAME: $DISTDATE"
 fi
 
 DISTPREFIX="$(cd "$DISTPREFIX"; pwd)"
 DISTBASE="$DISTPREFIX/dist-$DISTNAME"
 mkdir -p "$DISTBASE" || fail "Unable to create distribution base dir \"$DISTBASE\""
 
 DIR="$DISTBASE/$DISTNAME"
 [ -e "$DIR" ] && fail "Directory \"$DIR\" already exists"
 
 
 # retrieve repository archive
 
 echo "### Retrieving Mercurial repository $VERSION"
 
 "$HG" --repository "$ISABELLE_HOME" archive --type files -r "$IDENT" "$DIR" || \
   fail "Failed to retrieve $VERSION"
 
 rm -f "$DIR/.hg_archival.txt"
 rm -f "$DIR/.hgtags"
 rm -f "$DIR/.hgignore"
 rm -f "$DIR/README_REPOSITORY"
 
 
 # partial context switch to new version
 
 cd "$DIR"
 
 unset ISABELLE_SETTINGS_PRESENT
 unset ISABELLE_SITE_SETTINGS_PRESENT
 
 if [ -z "$RELEASE" ]; then
   {
     echo
     echo "IMPORTANT NOTE"
     echo "=============="
     echo
     echo "This is a snapshot of Isabelle/${IDENT} from the repository."
     echo
   } >ANNOUNCE
+fi
+
+if [ -n "$RELEASE" -a "$OFFICIAL_RELEASE" = true ]; then
+  IS_OFFICIAL="true"
 else
-  perl -pi -e "s,val is_official = false,val is_official = true,g" src/Pure/ROOT.ML
+  IS_OFFICIAL="false"
 fi
 
+perl -pi \
+  -e "s,val is_identified = false,val is_identified = true,g" \
+  -e "s,val is_official = false,val is_official = ${IS_OFFICIAL},g" \
+  src/Pure/ROOT.ML src/Pure/ROOT.scala
+
 perl -pi -e "s,ISABELLE_ID=\"\",ISABELLE_ID=\"$IDENT\",g" lib/scripts/getsettings
 perl -pi -e "s,ISABELLE_IDENTIFIER=\"\",ISABELLE_IDENTIFIER=\"$DISTNAME\",g" lib/scripts/getsettings
 perl -pi -e "s,{ISABELLE},$DISTNAME,g" lib/html/library_index_header.template
-perl -pi -e "s,unidentified repository version,$DISTVERSION,g" src/Pure/ROOT.ML lib/Tools/version
+perl -pi -e "s,unidentified repository version,$DISTVERSION,g" src/Pure/ROOT.ML src/Pure/ROOT.scala lib/Tools/version
 perl -pi -e "s,some unidentified repository version of Isabelle,$DISTVERSION,g" README
 
 mkdir -p contrib
 cat >contrib/README <<EOF
 This directory contains add-on components that contribute to the main
 Isabelle distribution.  Separate licensing conditions apply, see each
 directory individually.
 EOF
 
 
 # prepare dist for release
 
 echo "### Preparing distribution $DISTNAME"
 
 find . "(" -name \*.thy -o -name \*.ML -o -name \*.scala ")" -perm +111 -print | xargs chmod -f -x
 find . -print | xargs chmod -f u+rw
 
 export CLASSPATH="$ISABELLE_CLASSPATH"
 
 ./bin/isabelle env ISABELLE_SCALA_BUILD_OPTIONS="$ISABELLE_SCALA_BUILD_OPTIONS -optimise" \
   ./Admin/build all || fail "Failed to build distribution"
 
 ./bin/isabelle env ISABELLE_SCALA_BUILD_OPTIONS="$ISABELLE_SCALA_BUILD_OPTIONS -optimise" \
   ./bin/isabelle jedit -b || fail "Failed to build Isabelle/jEdit"
 
 cp -a src src.orig
 env ISABELLE_IDENTIFIER="${DISTNAME}-build" \
   ./bin/isabelle build_doc $JOBS -s -a || fail "Failed to build documentation"
 rm -rf src
 mv src.orig src
 
 rm -rf Admin browser_info heaps
 
 
 # create archive
 
 echo "### Creating archive"
 
 cd "$DISTBASE"
 
 echo "$DISTBASE/$DISTNAME.tar.gz" > ../ISABELLE_DIST
 echo "$IDENT" >../ISABELLE_IDENT
 
 chown -R "$LOGNAME" "$DISTNAME"
 chmod -R u+w "$DISTNAME"
 chmod -R g=o "$DISTNAME"
 
 echo "$DISTBASE/$DISTNAME.tar.gz"
 tar -c -z -f "$DISTNAME.tar.gz" "$DISTNAME"
 [ "$?" = 0 ] || exit "$?"
 
 
 # cleanup dist
 
 mv "$DISTNAME" "${DISTNAME}-old"
 mkdir "$DISTNAME"
 
 mv "${DISTNAME}-old/README" "${DISTNAME}-old/NEWS" "${DISTNAME}-old/ANNOUNCE" \
   "${DISTNAME}-old/COPYRIGHT" "${DISTNAME}-old/CONTRIBUTORS" "$DISTNAME"
 mkdir "$DISTNAME/doc"
 mv "${DISTNAME}-old/doc/"*.pdf "${DISTNAME}-old/doc/Contents" "$DISTNAME/doc"
 
 rm -f Isabelle && ln -sf "$DISTNAME" Isabelle
 
 rm -rf "${DISTNAME}-old"
 
diff --git a/src/Pure/PIDE/session.ML b/src/Pure/PIDE/session.ML
--- a/src/Pure/PIDE/session.ML
+++ b/src/Pure/PIDE/session.ML
@@ -1,80 +1,80 @@
 (*  Title:      Pure/PIDE/session.ML
     Author:     Makarius
 
 Prover session: persistent state of logic image.
 *)
 
 signature SESSION =
 sig
   val name: unit -> string
   val welcome: unit -> string
   val init: bool -> bool -> Path.T -> string -> bool -> string -> (string * string) list ->
     (Path.T * Path.T) list -> string -> string * string -> bool -> unit
   val finish: unit -> unit
   val protocol_handler: string -> unit
   val init_protocol_handlers: unit -> unit
 end;
 
 structure Session: SESSION =
 struct
 
 (** session identification -- not thread-safe **)
 
 val session = Unsynchronized.ref {chapter = "Pure", name = "Pure"};
 val session_finished = Unsynchronized.ref false;
 
 fun name () = "Isabelle/" ^ #name (! session);
 
 fun welcome () =
-  if Distribution.is_official then
+  if Distribution.is_identified then
     "Welcome to " ^ name () ^ " (" ^ Distribution.version ^ ")"
   else "Unofficial version of " ^ name () ^ " (" ^ Distribution.version ^ ")";
 
 
 (* init *)
 
 fun init build info info_path doc doc_graph doc_output doc_variants doc_files
     parent (chapter, name) verbose =
   if #name (! session) <> parent orelse not (! session_finished) then
     error ("Unfinished parent session " ^ quote parent ^ " for " ^ quote name)
   else
     let
       val _ = session := {chapter = chapter, name = name};
       val _ = session_finished := false;
     in
       Present.init build info info_path (if doc = "false" then "" else doc)
         doc_graph doc_output doc_variants doc_files (chapter, name)
         verbose (map Thy_Info.get_theory (Thy_Info.get_names ()))
     end;
 
 
 (* finish *)
 
 fun finish () =
  (Execution.shutdown ();
   Thy_Info.finish ();
   Present.finish ();
   Outer_Syntax.check_syntax ();
   Future.shutdown ();
   Event_Timer.shutdown ();
   Future.shutdown ();
   session_finished := true);
 
 
 
 (** protocol handlers **)
 
 val protocol_handlers = Synchronized.var "protocol_handlers" ([]: string list);
 
 fun protocol_handler name =
   Synchronized.change protocol_handlers (fn handlers =>
    (Output.try_protocol_message (Markup.protocol_handler name) [];
     if not (member (op =) handlers name) then ()
     else warning ("Redefining protocol handler: " ^ quote name);
     update (op =) name handlers));
 
 fun init_protocol_handlers () =
   Synchronized.value protocol_handlers
   |> List.app (fn name => Output.try_protocol_message (Markup.protocol_handler name) []);
 
 end;
diff --git a/src/Pure/ROOT.ML b/src/Pure/ROOT.ML
--- a/src/Pure/ROOT.ML
+++ b/src/Pure/ROOT.ML
@@ -1,379 +1,380 @@
 (*** Isabelle/Pure bootstrap from "RAW" environment ***)
 
 (** bootstrap phase 0: towards secure ML barrier *)
 
 structure Distribution =     (*filled-in by makedist*)
 struct
   val version = "unidentified repository version";
+  val is_identified = false;
   val is_official = false;
 end;
 
 
 (* library of general tools *)
 
 use "General/basics.ML";
 use "library.ML";
 use "General/print_mode.ML";
 use "General/alist.ML";
 use "General/table.ML";
 
 use "Concurrent/simple_thread.ML";
 
 use "Concurrent/synchronized.ML";
 if Multithreading.available then ()
 else use "Concurrent/synchronized_sequential.ML";
 use "Concurrent/counter.ML";
 
 use "General/properties.ML";
 use "General/output.ML";
 use "PIDE/markup.ML";
 fun legacy_feature s = warning (Markup.markup Markup.legacy ("Legacy feature! " ^ s));
 use "General/scan.ML";
 use "General/source.ML";
 use "General/symbol.ML";
 use "General/position.ML";
 use "General/symbol_pos.ML";
 use "General/antiquote.ML";
 use "ML/ml_lex.ML";
 use "ML/ml_parse.ML";
 use "General/secure.ML";
 
 val use_text = Secure.use_text;
 val use_file = Secure.use_file;
 
 fun use s =
   Position.setmp_thread_data (Position.file_only s)
     (fn () =>
       Secure.use_file ML_Parse.global_context true s
         handle ERROR msg => (writeln msg; error "ML error")) ();
 
 val toplevel_pp = Secure.toplevel_pp;
 
 
 (** bootstrap phase 1: towards ML within Isar context *)
 
 (* library of general tools *)
 
 use "General/integer.ML";
 use "General/stack.ML";
 use "General/queue.ML";
 use "General/heap.ML";
 use "General/same.ML";
 use "General/ord_list.ML";
 use "General/balanced_tree.ML";
 use "General/linear_set.ML";
 use "General/buffer.ML";
 use "General/pretty.ML";
 use "General/path.ML";
 use "General/url.ML";
 use "General/file.ML";
 use "General/long_name.ML";
 use "General/binding.ML";
 use "General/socket_io.ML";
 use "General/seq.ML";
 use "General/timing.ML";
 
 use "General/sha1.ML";
 if ML_System.is_polyml then use "General/sha1_polyml.ML" else ();
 use "General/sha1_samples.ML";
 
 use "PIDE/xml.ML";
 use "PIDE/yxml.ML";
 use "PIDE/document_id.ML";
 
 use "General/change_table.ML";
 use "General/graph.ML";
 
 use "System/options.ML";
 
 
 (* concurrency within the ML runtime *)
 
 if ML_System.is_polyml
 then use "ML/exn_properties_polyml.ML"
 else use "ML/exn_properties_dummy.ML";
 
 if ML_System.name = "polyml-5.5.1"
   orelse ML_System.name = "polyml-5.5.2"
 then use "ML/exn_trace_polyml-5.5.1.ML"
 else ();
 
 if ML_System.name = "polyml-5.5.0"
   orelse ML_System.name = "polyml-5.5.1"
   orelse ML_System.name = "polyml-5.5.2"
 then use "ML/ml_statistics_polyml-5.5.0.ML"
 else use "ML/ml_statistics_dummy.ML";
 
 use "Concurrent/single_assignment.ML";
 if Multithreading.available then ()
 else use "Concurrent/single_assignment_sequential.ML";
 
 if Multithreading.available
 then use "Concurrent/bash.ML"
 else use "Concurrent/bash_sequential.ML";
 
 use "Concurrent/par_exn.ML";
 use "Concurrent/task_queue.ML";
 use "Concurrent/future.ML";
 use "Concurrent/event_timer.ML";
 
 if ML_System.is_polyml then use "Concurrent/time_limit.ML" else ();
 
 use "Concurrent/lazy.ML";
 if Multithreading.available then ()
 else use "Concurrent/lazy_sequential.ML";
 
 use "Concurrent/par_list.ML";
 if Multithreading.available then ()
 else use "Concurrent/par_list_sequential.ML";
 
 use "Concurrent/mailbox.ML";
 use "Concurrent/cache.ML";
 
 use "PIDE/active.ML";
 
 
 (* fundamental structures *)
 
 use "name.ML";
 use "term.ML";
 use "context.ML";
 use "context_position.ML";
 use "config.ML";
 
 
 (* inner syntax *)
 
 use "Syntax/type_annotation.ML";
 use "Syntax/term_position.ML";
 use "Syntax/lexicon.ML";
 use "Syntax/ast.ML";
 use "Syntax/syntax_ext.ML";
 use "Syntax/parser.ML";
 use "Syntax/syntax_trans.ML";
 use "Syntax/mixfix.ML";
 use "Syntax/printer.ML";
 use "Syntax/syntax.ML";
 
 
 (* core of tactical proof system *)
 
 use "term_ord.ML";
 use "term_subst.ML";
 use "term_xml.ML";
 use "General/completion.ML";
 use "General/name_space.ML";
 use "sorts.ML";
 use "type.ML";
 use "logic.ML";
 use "Syntax/simple_syntax.ML";
 use "net.ML";
 use "item_net.ML";
 use "envir.ML";
 use "consts.ML";
 use "primitive_defs.ML";
 use "defs.ML";
 use "sign.ML";
 use "term_sharing.ML";
 use "pattern.ML";
 use "unify.ML";
 use "theory.ML";
 use "interpretation.ML";
 use "proofterm.ML";
 use "thm.ML";
 use "more_thm.ML";
 use "facts.ML";
 use "global_theory.ML";
 use "pure_thy.ML";
 use "drule.ML";
 use "morphism.ML";
 use "variable.ML";
 use "conv.ML";
 use "goal_display.ML";
 use "tactical.ML";
 use "search.ML";
 use "tactic.ML";
 use "raw_simplifier.ML";
 use "conjunction.ML";
 use "assumption.ML";
 use "display.ML";
 
 
 (* Isar -- Intelligible Semi-Automated Reasoning *)
 
 (*ML support and global execution*)
 use "ML/ml_syntax.ML";
 use "ML/ml_env.ML";
 use "ML/ml_options.ML";
 use "ML/exn_output.ML";
 if ML_System.is_polyml then use "ML/exn_output_polyml.ML" else ();
 use "ML/ml_options.ML";
 use "Isar/runtime.ML";
 use "PIDE/execution.ML";
 use "ML/ml_compiler.ML";
 if ML_System.is_polyml then use "ML/ml_compiler_polyml.ML" else ();
 
 use "skip_proof.ML";
 use "goal.ML";
 
 (*proof context*)
 use "Isar/object_logic.ML";
 use "Isar/rule_cases.ML";
 use "Isar/auto_bind.ML";
 use "type_infer.ML";
 use "Syntax/local_syntax.ML";
 use "Isar/proof_context.ML";
 use "type_infer_context.ML";
 use "Syntax/syntax_phases.ML";
 use "Isar/local_defs.ML";
 
 (*outer syntax*)
 use "Isar/token.ML";
 use "Isar/keyword.ML";
 use "Isar/parse.ML";
 use "Isar/args.ML";
 
 (*theory sources*)
 use "Thy/thy_header.ML";
 use "Thy/thy_syntax.ML";
 use "Thy/html.ML";
 use "Thy/latex.ML";
 
 (*ML with context and antiquotations*)
 use "ML/ml_context.ML";
 use "ML/ml_antiquotation.ML";
 
 fun use s =
   ML_Context.eval_file (ML_Compiler.verbose true ML_Compiler.flags) (Path.explode s)
     handle ERROR msg => (writeln msg; error "ML error");
 
 
 
 (** bootstrap phase 2: towards Pure.thy and final ML toplevel setup *)
 
 (*basic proof engine*)
 use "Isar/proof_display.ML";
 use "Isar/attrib.ML";
 use "Isar/context_rules.ML";
 use "Isar/method.ML";
 use "Isar/proof.ML";
 use "Isar/element.ML";
 use "Isar/obtain.ML";
 
 (*local theories and targets*)
 use "Isar/locale.ML";
 use "Isar/local_theory.ML";
 use "Isar/generic_target.ML";
 use "Isar/overloading.ML";
 use "axclass.ML";
 use "Isar/class.ML";
 use "Isar/named_target.ML";
 use "Isar/expression.ML";
 use "Isar/class_declaration.ML";
 use "Isar/bundle.ML";
 
 use "simplifier.ML";
 
 (*executable theory content*)
 use "Isar/code.ML";
 
 (*specifications*)
 use "Isar/parse_spec.ML";
 use "Isar/spec_rules.ML";
 use "Isar/specification.ML";
 use "Isar/typedecl.ML";
 
 (*toplevel transactions*)
 use "Isar/proof_node.ML";
 use "Isar/toplevel.ML";
 
 (*proof term operations*)
 use "Proof/reconstruct.ML";
 use "Proof/proof_syntax.ML";
 use "Proof/proof_rewrite_rules.ML";
 use "Proof/proof_checker.ML";
 use "Proof/extraction.ML";
 
 (*theory documents*)
 use "System/isabelle_system.ML";
 use "Thy/term_style.ML";
 use "Thy/thy_output.ML";
 use "Isar/outer_syntax.ML";
 use "General/graph_display.ML";
 use "Thy/present.ML";
 use "PIDE/command.ML";
 use "PIDE/query_operation.ML";
 use "PIDE/resources.ML";
 use "Thy/thy_info.ML";
 use "PIDE/document.ML";
 
 (*theory and proof operations*)
 use "Thy/thm_deps.ML";
 use "Isar/isar_cmd.ML";
 
 use "subgoal.ML";
 
 
 (* Isabelle/Isar system *)
 
 use "PIDE/session.ML";
 use "System/command_line.ML";
 use "System/system_channel.ML";
 use "System/message_channel.ML";
 use "System/isabelle_process.ML";
 use "System/invoke_scala.ML";
 use "PIDE/protocol.ML";
 use "System/isar.ML";
 
 
 (* miscellaneous tools and packages for Pure Isabelle *)
 
 use "Tools/build.ML";
 use "Tools/named_thms.ML";
 use "Tools/proof_general.ML";
 
 structure Output: OUTPUT = Output;  (*seal system channels!*)
 
 
 (* ML toplevel pretty printing *)
 
 toplevel_pp ["Pretty", "T"] "(fn _: Pretty.T => Pretty.str \"<pretty>\")";
 toplevel_pp ["Task_Queue", "task"] "Pretty.str o Task_Queue.str_of_task";
 toplevel_pp ["Task_Queue", "group"] "Pretty.str o Task_Queue.str_of_group";
 toplevel_pp ["Position", "T"] "Pretty.position";
 toplevel_pp ["Binding", "binding"] "Pretty.str o Binding.print";
 toplevel_pp ["Thm", "thm"] "Proof_Display.pp_thm";
 toplevel_pp ["Thm", "cterm"] "Proof_Display.pp_cterm";
 toplevel_pp ["Thm", "ctyp"] "Proof_Display.pp_ctyp";
 toplevel_pp ["Context", "theory"] "Context.pretty_thy";
 toplevel_pp ["Context", "Proof", "context"] "Proof_Display.pp_context";
 toplevel_pp ["Ast", "ast"] "Ast.pretty_ast";
 toplevel_pp ["Path", "T"] "Path.pretty";
 toplevel_pp ["SHA1", "digest"] "Pretty.str o quote o SHA1.rep";
 toplevel_pp ["Proof", "state"] "(fn _: Proof.state => Pretty.str \"<Proof.state>\")";
 toplevel_pp ["Toplevel", "state"] "Toplevel.pretty_abstract";
 toplevel_pp ["Morphism", "morphism"] "Morphism.pretty";
 
 if ML_System.is_polyml then use "ML/install_pp_polyml.ML" else ();
 
 
 (* the Pure theory *)
 
 use "pure_syn.ML";
 Runtime.toplevel_program (fn () => Thy_Info.use_thy ("Pure", Position.none));
 Context.set_thread_data NONE;
 structure Pure = struct val thy = Thy_Info.get_theory "Pure" end;
 
 toplevel_pp ["typ"] "Proof_Display.pp_typ Pure.thy";
 
 
 (* ML toplevel commands *)
 
 fun use_thys args =
   Runtime.toplevel_program (fn () => Thy_Info.use_thys (map (rpair Position.none) args));
 val use_thy = use_thys o single;
 
 val cd = File.cd o Path.explode;
 
 Proofterm.proofs := 0;
 
diff --git a/src/Pure/ROOT.scala b/src/Pure/ROOT.scala
--- a/src/Pure/ROOT.scala
+++ b/src/Pure/ROOT.scala
@@ -1,11 +1,17 @@
 /*  Title:      Pure/ROOT.scala
     Module:     PIDE
     Author:     Makarius
 
 Root of isabelle package.
 */
 
 package object isabelle extends isabelle.Basic_Library
 {
+  object Distribution     /*filled-in by makedist*/
+  {
+    val version = "unidentified repository version"
+    val is_identified = false
+    val is_official = false
+  }
 }
 
diff --git a/src/Tools/jEdit/src/plugin.scala b/src/Tools/jEdit/src/plugin.scala
--- a/src/Tools/jEdit/src/plugin.scala
+++ b/src/Tools/jEdit/src/plugin.scala
@@ -1,413 +1,420 @@
 /*  Title:      Tools/jEdit/src/plugin.scala
     Author:     Makarius
 
 Main plumbing for PIDE infrastructure as jEdit plugin.
 */
 
 package isabelle.jedit
 
 
 import isabelle._
 
 import javax.swing.JOptionPane
 
 import scala.swing.{ListView, ScrollPane}
 
 import org.gjt.sp.jedit.{jEdit, EBMessage, EBPlugin, Buffer, View, Debug}
 import org.jedit.options.CombinedOptions
 import org.gjt.sp.jedit.gui.AboutDialog
 import org.gjt.sp.jedit.textarea.{JEditTextArea, TextArea}
 import org.gjt.sp.jedit.syntax.ModeProvider
 import org.gjt.sp.jedit.msg.{EditorStarted, BufferUpdate, EditPaneUpdate, PropertiesChanged}
 
 import org.gjt.sp.util.SyntaxUtilities
 
 
 object PIDE
 {
   /* plugin instance */
 
   val options = new JEdit_Options
   val completion_history = new Completion.History_Variable
   val spell_checker = new Spell_Checker_Variable
 
   @volatile var startup_failure: Option[Throwable] = None
   @volatile var startup_notified = false
 
   @volatile var plugin: Plugin = null
   @volatile var session: Session =
     new Session(new JEdit_Resources(Set.empty, Map.empty, Outer_Syntax.empty))
 
   def options_changed() { plugin.options_changed() }
   def deps_changed() { plugin.deps_changed() }
 
   def resources(): JEdit_Resources =
     session.resources.asInstanceOf[JEdit_Resources]
 
   lazy val editor = new JEdit_Editor
 
 
   /* popups */
 
   def dismissed_popups(view: View): Boolean =
   {
     var dismissed = false
 
     JEdit_Lib.jedit_text_areas(view).foreach(text_area =>
       if (Completion_Popup.Text_Area.dismissed(text_area)) dismissed = true)
 
     if (Pretty_Tooltip.dismissed_all()) dismissed = true
 
     dismissed
   }
 
 
   /* document model and view */
 
   def document_model(buffer: Buffer): Option[Document_Model] = Document_Model(buffer)
 
   def document_view(text_area: TextArea): Option[Document_View] = Document_View(text_area)
 
   def document_views(buffer: Buffer): List[Document_View] =
     for {
       text_area <- JEdit_Lib.jedit_text_areas(buffer).toList
       doc_view <- document_view(text_area)
     } yield doc_view
 
   def document_models(): List[Document_Model] =
     for {
       buffer <- JEdit_Lib.jedit_buffers().toList
       model <- document_model(buffer)
     } yield model
 
   def document_blobs(): Document.Blobs =
     Document.Blobs(
       (for {
         buffer <- JEdit_Lib.jedit_buffers()
         model <- document_model(buffer)
         blob <- model.get_blob()
       } yield (model.node_name -> blob)).toMap)
 
   def exit_models(buffers: List[Buffer])
   {
     GUI_Thread.now {
       PIDE.editor.flush()
       buffers.foreach(buffer =>
         JEdit_Lib.buffer_lock(buffer) {
           JEdit_Lib.jedit_text_areas(buffer).foreach(Document_View.exit)
           Document_Model.exit(buffer)
         })
       }
   }
 
   def init_models()
   {
     GUI_Thread.now {
       PIDE.editor.flush()
 
       for {
         buffer <- JEdit_Lib.jedit_buffers()
         if buffer != null && !buffer.isLoading && !buffer.getBooleanProperty(Buffer.GZIPPED)
       } {
         JEdit_Lib.buffer_lock(buffer) {
           val node_name = resources.node_name(buffer)
           val model =
             document_model(buffer) match {
               case Some(model) if model.node_name == node_name => model
               case _ => Document_Model.init(session, buffer, node_name)
             }
           for {
             text_area <- JEdit_Lib.jedit_text_areas(buffer)
             if document_view(text_area).map(_.model) != Some(model)
           } Document_View.init(model, text_area)
         }
       }
 
       PIDE.editor.invoke()
     }
   }
 
   def init_view(buffer: Buffer, text_area: JEditTextArea): Unit =
     GUI_Thread.now {
       JEdit_Lib.buffer_lock(buffer) {
         document_model(buffer) match {
           case Some(model) => Document_View.init(model, text_area)
           case None =>
         }
       }
     }
 
   def exit_view(buffer: Buffer, text_area: JEditTextArea): Unit =
     GUI_Thread.now {
       JEdit_Lib.buffer_lock(buffer) {
         Document_View.exit(text_area)
       }
     }
 
 
   /* current document content */
 
   def snapshot(view: View): Document.Snapshot = GUI_Thread.now
   {
     val buffer = view.getBuffer
     document_model(buffer) match {
       case Some(model) => model.snapshot
       case None => error("No document model for current buffer")
     }
   }
 
   def rendering(view: View): Rendering = GUI_Thread.now
   {
     val text_area = view.getTextArea
     document_view(text_area) match {
       case Some(doc_view) => doc_view.get_rendering()
       case None => error("No document view for current text area")
     }
   }
 }
 
 
 class Plugin extends EBPlugin
 {
   /* global changes */
 
   def options_changed()
   {
     PIDE.session.global_options.post(Session.Global_Options(PIDE.options.value))
     delay_load.invoke()
   }
 
   def deps_changed()
   {
     delay_load.invoke()
   }
 
 
   /* theory files */
 
   private lazy val delay_init =
     GUI_Thread.delay_last(PIDE.options.seconds("editor_load_delay"))
     {
       PIDE.init_models()
     }
 
   private val delay_load_active = Synchronized(false)
   private def delay_load_activated(): Boolean =
     delay_load_active.guarded_access(a => Some((!a, true)))
 
   private lazy val delay_load =
     GUI_Thread.delay_last(PIDE.options.seconds("editor_load_delay"))
     {
       if (Isabelle.continuous_checking && delay_load_activated()) {
         try {
           val view = jEdit.getActiveView()
 
           val buffers = JEdit_Lib.jedit_buffers().toList
           if (buffers.forall(_.isLoaded)) {
             def loaded_buffer(name: String): Boolean =
               buffers.exists(buffer => JEdit_Lib.buffer_name(buffer) == name)
 
             val thys =
               for {
                 buffer <- buffers
                 model <- PIDE.document_model(buffer)
                 if model.is_theory
               } yield (model.node_name, Position.none)
 
             val thy_info = new Thy_Info(PIDE.resources)
             // FIXME avoid I/O on GUI thread!?!
             val files = thy_info.dependencies("", thys).deps.map(_.name.node).
               filter(file => !loaded_buffer(file) && PIDE.resources.check_file(view, file))
 
             if (!files.isEmpty) {
               if (PIDE.options.bool("jedit_auto_load")) {
                 files.foreach(file => jEdit.openFile(null: View, file))
               }
               else {
                 val files_list = new ListView(files.sorted)
                 for (i <- 0 until files.length)
                   files_list.selection.indices += i
 
                 val answer =
                   GUI.confirm_dialog(view,
                     "Auto loading of required files",
                     JOptionPane.YES_NO_OPTION,
                     "The following files are required to resolve theory imports.",
                     "Reload selected files now?",
                     new ScrollPane(files_list),
                     new Isabelle.Continuous_Checking)
                 if (answer == 0) {
                   files.foreach(file =>
                     if (files_list.selection.items.contains(file))
                       jEdit.openFile(null: View, file))
                 }
               }
             }
           }
         }
         finally { delay_load_active.change(_ => false) }
       }
     }
 
 
   /* session phase */
 
   private val session_phase =
     Session.Consumer[Session.Phase](getClass.getName) {
       case Session.Inactive | Session.Failed =>
         GUI_Thread.later {
           GUI.error_dialog(jEdit.getActiveView, "Prover process terminated",
             "Isabelle Syslog", GUI.scrollable_text(PIDE.session.syslog_content()))
         }
 
       case Session.Ready =>
         PIDE.session.update_options(PIDE.options.value)
         PIDE.init_models()
 
         if (!Isabelle.continuous_checking) {
           GUI_Thread.later {
             val answer =
               GUI.confirm_dialog(jEdit.getActiveView,
                 "Continuous checking of PIDE document",
                 JOptionPane.YES_NO_OPTION,
                 "Continuous checking is presently disabled:",
                 "editor buffers will remain inactive!",
                 "Enable continuous checking now?")
             if (answer == 0) Isabelle.continuous_checking = true
           }
         }
 
         delay_load.invoke()
 
       case Session.Shutdown =>
         PIDE.exit_models(JEdit_Lib.jedit_buffers().toList)
         delay_load.revoke()
 
       case _ =>
     }
 
 
   /* main plugin plumbing */
 
   override def handleMessage(message: EBMessage)
   {
     GUI_Thread.assert {}
 
     if (PIDE.startup_failure.isDefined && !PIDE.startup_notified) {
       message match {
         case msg: EditorStarted =>
           GUI.error_dialog(null, "Isabelle plugin startup failure",
             GUI.scrollable_text(Exn.message(PIDE.startup_failure.get)),
             "Prover IDE inactive!")
           PIDE.startup_notified = true
         case _ =>
       }
     }
 
     if (PIDE.startup_failure.isEmpty) {
       message match {
         case msg: EditorStarted =>
           PIDE.session.start("Isabelle", Isabelle_Logic.session_args())
 
+          if (Distribution.is_identified && !Distribution.is_official) {
+            GUI.warning_dialog(jEdit.getActiveView, "Isabelle release candidate for testing",
+              "This is " + Distribution.version +".",
+              "It is for testing only, not for production use.")
+          }
+
+
         case msg: BufferUpdate
         if msg.getWhat == BufferUpdate.LOADED ||
           msg.getWhat == BufferUpdate.PROPERTIES_CHANGED ||
           msg.getWhat == BufferUpdate.CLOSING =>
 
           if (msg.getWhat == BufferUpdate.CLOSING) {
             val buffer = msg.getBuffer
             if (buffer != null) PIDE.editor.remove_node(PIDE.resources.node_name(msg.getBuffer))
           }
           if (PIDE.session.is_ready) {
             delay_init.invoke()
             delay_load.invoke()
           }
 
         case msg: EditPaneUpdate
         if (msg.getWhat == EditPaneUpdate.BUFFER_CHANGING ||
             msg.getWhat == EditPaneUpdate.BUFFER_CHANGED ||
             msg.getWhat == EditPaneUpdate.CREATED ||
             msg.getWhat == EditPaneUpdate.DESTROYED) =>
           val edit_pane = msg.getEditPane
           val buffer = edit_pane.getBuffer
           val text_area = edit_pane.getTextArea
 
           if (buffer != null && text_area != null) {
             if (msg.getWhat == EditPaneUpdate.BUFFER_CHANGED ||
                 msg.getWhat == EditPaneUpdate.CREATED) {
               if (PIDE.session.is_ready)
                 PIDE.init_view(buffer, text_area)
             }
             else {
               PIDE.dismissed_popups(text_area.getView)
               PIDE.exit_view(buffer, text_area)
             }
 
             if (msg.getWhat == EditPaneUpdate.CREATED)
               Completion_Popup.Text_Area.init(text_area)
 
             if (msg.getWhat == EditPaneUpdate.DESTROYED)
               Completion_Popup.Text_Area.exit(text_area)
           }
 
         case msg: PropertiesChanged =>
           PIDE.spell_checker.update(PIDE.options.value)
           PIDE.session.update_options(PIDE.options.value)
 
         case _ =>
       }
     }
   }
 
   override def start()
   {
     try {
       Debug.DISABLE_SEARCH_DIALOG_POOL = true
 
       PIDE.plugin = this
       Isabelle_System.init()
       Isabelle_Font.install_fonts()
 
       PIDE.options.update(Options.init())
       PIDE.completion_history.load()
       PIDE.spell_checker.update(PIDE.options.value)
 
       SyntaxUtilities.setStyleExtender(new Token_Markup.Style_Extender)
       if (ModeProvider.instance.isInstanceOf[ModeProvider])
         ModeProvider.instance = new Token_Markup.Mode_Provider(ModeProvider.instance)
 
       JEdit_Lib.jedit_text_areas.foreach(Completion_Popup.Text_Area.init _)
 
       val content = Isabelle_Logic.session_content(false)
       val resources =
         new JEdit_Resources(content.loaded_theories, content.known_theories, content.syntax)
 
       PIDE.session = new Session(resources) {
         override def output_delay = PIDE.options.seconds("editor_output_delay")
         override def reparse_limit = PIDE.options.int("editor_reparse_limit")
       }
 
       PIDE.session.phase_changed += session_phase
       PIDE.startup_failure = None
     }
     catch {
       case exn: Throwable =>
         PIDE.startup_failure = Some(exn)
         PIDE.startup_notified = false
     }
   }
 
   override def stop()
   {
     JEdit_Lib.jedit_text_areas.foreach(Completion_Popup.Text_Area.exit _)
 
     if (PIDE.startup_failure.isEmpty) {
       PIDE.options.value.save_prefs()
       PIDE.completion_history.value.save()
     }
 
     PIDE.session.phase_changed -= session_phase
     PIDE.exit_models(JEdit_Lib.jedit_buffers().toList)
     PIDE.session.stop()
   }
 }