# HG changeset patch
# User wenzelm
# Date 1368359201 -7200
# Node ID cf9c8d8d89395ae3166f0bb903d1ddb55a34563f
# Parent  db22d73e6c3e8774df95a290afa31f1bbe9afadc
Proof General interaction always uses Isar loop;
pass Isabelle/Scala options to Proof General process as well;

diff -r db22d73e6c3e -r cf9c8d8d8939 bin/isabelle-process
--- a/bin/isabelle-process	Sun May 12 13:08:23 2013 +0200
+++ b/bin/isabelle-process	Sun May 12 13:46:41 2013 +0200
@@ -76,6 +76,7 @@
       ISAR=true
       ;;
     P)
+      ISAR=true
       PROOFGENERAL=true
       ;;
     S)
@@ -221,14 +222,16 @@
   [ -p "${FIFOS[0]}" ] || fail "Bad input fifo: ${FIFOS[0]}"
   [ -p "${FIFOS[1]}" ] || fail "Bad output fifo: ${FIFOS[1]}"
   MLTEXT="$MLTEXT; Isabelle_Process.init_fifos \"${FIFOS[0]}\" \"${FIFOS[1]}\";"
-elif [ -n "$PROOFGENERAL" ]; then
-  MLTEXT="$MLTEXT; ProofGeneral.init $ISAR;"
 elif [ "$ISAR" = true ]; then
   if [ -z "$ISABELLE_PROCESS_OPTIONS" ]; then
     ISABELLE_PROCESS_OPTIONS="$ISABELLE_TMP/options"
     "$ISABELLE_TOOL" options -x "$ISABELLE_PROCESS_OPTIONS" || fail "Failed to retrieve options"
   fi
-  MLTEXT="$MLTEXT; Isar.main ();"
+  if [ -n "$PROOFGENERAL" ]; then
+    MLTEXT="$MLTEXT; ProofGeneral.init ();"
+  else
+    MLTEXT="$MLTEXT; Isar.main ();"
+  fi
 else
   NICE=""
 fi
diff -r db22d73e6c3e -r cf9c8d8d8939 src/Pure/ProofGeneral/proof_general_emacs.ML
--- a/src/Pure/ProofGeneral/proof_general_emacs.ML	Sun May 12 13:08:23 2013 +0200
+++ b/src/Pure/ProofGeneral/proof_general_emacs.ML	Sun May 12 13:46:41 2013 +0200
@@ -8,7 +8,7 @@
 signature PROOF_GENERAL =
 sig
   val test_markupN: string
-  val init: bool -> unit
+  val init: unit -> unit
   structure ThyLoad: sig val add_path: string -> unit end
 end;
 
@@ -92,9 +92,6 @@
   Output.Private_Hooks.error_fn := (fn (_, s) => message (special "M") (special "N") "*** " s);
   Output.Private_Hooks.prompt_fn := (fn s => Output.physical_stdout (render s ^ special "S")));
 
-fun panic s =
-  (message (special "M") (special "N") "!!! " ("## SYSTEM EXIT ##\n" ^ s); exit 1);
-
 
 (* notification *)
 
@@ -227,24 +224,23 @@
 
 val initialized = Unsynchronized.ref false;
 
-fun init false = panic "No Proof General interface support for Isabelle/classic mode."
-  | init true =
-      (if ! initialized then ()
-       else
-        (Output.add_mode Symbol.xsymbolsN Symbol.output Output.default_escape;
-         Output.add_mode ProofGeneralPgip.proof_general_emacsN
-          Output.default_output Output.default_escape;
-         Markup.add_mode ProofGeneralPgip.proof_general_emacsN YXML.output_markup;
-         setup_messages ();
-         ProofGeneralPgip.init_pgip_session_id ();
-         setup_thy_loader ();
-         setup_present_hook ();
-         initialized := true);
-       sync_thy_loader ();
-       Unsynchronized.change print_mode (update (op =) ProofGeneralPgip.proof_general_emacsN);
-       Secure.PG_setup ();
-       Isar.toplevel_loop TextIO.stdIn
-        {init = true, welcome = true, sync = true, secure = Secure.is_secure ()});
+fun init () =
+  (if ! initialized then ()
+   else
+    (Output.add_mode Symbol.xsymbolsN Symbol.output Output.default_escape;
+     Output.add_mode ProofGeneralPgip.proof_general_emacsN
+      Output.default_output Output.default_escape;
+     Markup.add_mode ProofGeneralPgip.proof_general_emacsN YXML.output_markup;
+     setup_messages ();
+     ProofGeneralPgip.init_pgip_session_id ();
+     setup_thy_loader ();
+     setup_present_hook ();
+     initialized := true);
+   sync_thy_loader ();
+   Unsynchronized.change print_mode (update (op =) ProofGeneralPgip.proof_general_emacsN);
+   Secure.PG_setup ();
+   Isar.toplevel_loop TextIO.stdIn
+    {init = true, welcome = true, sync = true, secure = Secure.is_secure ()});
 
 
 (* fake old ThyLoad -- with new semantics *)