Proof General interaction always uses Isar loop;
pass Isabelle/Scala options to Proof General process as well;
--- 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
--- 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 *)