Proof General interaction always uses Isar loop;
authorwenzelm
Sun May 12 13:46:41 2013 +0200 (2013-05-12)
changeset 51938cf9c8d8d8939
parent 51937 db22d73e6c3e
child 51939 65548ab2fc55
Proof General interaction always uses Isar loop;
pass Isabelle/Scala options to Proof General process as well;
bin/isabelle-process
src/Pure/ProofGeneral/proof_general_emacs.ML
     1.1 --- a/bin/isabelle-process	Sun May 12 13:08:23 2013 +0200
     1.2 +++ b/bin/isabelle-process	Sun May 12 13:46:41 2013 +0200
     1.3 @@ -76,6 +76,7 @@
     1.4        ISAR=true
     1.5        ;;
     1.6      P)
     1.7 +      ISAR=true
     1.8        PROOFGENERAL=true
     1.9        ;;
    1.10      S)
    1.11 @@ -221,14 +222,16 @@
    1.12    [ -p "${FIFOS[0]}" ] || fail "Bad input fifo: ${FIFOS[0]}"
    1.13    [ -p "${FIFOS[1]}" ] || fail "Bad output fifo: ${FIFOS[1]}"
    1.14    MLTEXT="$MLTEXT; Isabelle_Process.init_fifos \"${FIFOS[0]}\" \"${FIFOS[1]}\";"
    1.15 -elif [ -n "$PROOFGENERAL" ]; then
    1.16 -  MLTEXT="$MLTEXT; ProofGeneral.init $ISAR;"
    1.17  elif [ "$ISAR" = true ]; then
    1.18    if [ -z "$ISABELLE_PROCESS_OPTIONS" ]; then
    1.19      ISABELLE_PROCESS_OPTIONS="$ISABELLE_TMP/options"
    1.20      "$ISABELLE_TOOL" options -x "$ISABELLE_PROCESS_OPTIONS" || fail "Failed to retrieve options"
    1.21    fi
    1.22 -  MLTEXT="$MLTEXT; Isar.main ();"
    1.23 +  if [ -n "$PROOFGENERAL" ]; then
    1.24 +    MLTEXT="$MLTEXT; ProofGeneral.init ();"
    1.25 +  else
    1.26 +    MLTEXT="$MLTEXT; Isar.main ();"
    1.27 +  fi
    1.28  else
    1.29    NICE=""
    1.30  fi
     2.1 --- a/src/Pure/ProofGeneral/proof_general_emacs.ML	Sun May 12 13:08:23 2013 +0200
     2.2 +++ b/src/Pure/ProofGeneral/proof_general_emacs.ML	Sun May 12 13:46:41 2013 +0200
     2.3 @@ -8,7 +8,7 @@
     2.4  signature PROOF_GENERAL =
     2.5  sig
     2.6    val test_markupN: string
     2.7 -  val init: bool -> unit
     2.8 +  val init: unit -> unit
     2.9    structure ThyLoad: sig val add_path: string -> unit end
    2.10  end;
    2.11  
    2.12 @@ -92,9 +92,6 @@
    2.13    Output.Private_Hooks.error_fn := (fn (_, s) => message (special "M") (special "N") "*** " s);
    2.14    Output.Private_Hooks.prompt_fn := (fn s => Output.physical_stdout (render s ^ special "S")));
    2.15  
    2.16 -fun panic s =
    2.17 -  (message (special "M") (special "N") "!!! " ("## SYSTEM EXIT ##\n" ^ s); exit 1);
    2.18 -
    2.19  
    2.20  (* notification *)
    2.21  
    2.22 @@ -227,24 +224,23 @@
    2.23  
    2.24  val initialized = Unsynchronized.ref false;
    2.25  
    2.26 -fun init false = panic "No Proof General interface support for Isabelle/classic mode."
    2.27 -  | init true =
    2.28 -      (if ! initialized then ()
    2.29 -       else
    2.30 -        (Output.add_mode Symbol.xsymbolsN Symbol.output Output.default_escape;
    2.31 -         Output.add_mode ProofGeneralPgip.proof_general_emacsN
    2.32 -          Output.default_output Output.default_escape;
    2.33 -         Markup.add_mode ProofGeneralPgip.proof_general_emacsN YXML.output_markup;
    2.34 -         setup_messages ();
    2.35 -         ProofGeneralPgip.init_pgip_session_id ();
    2.36 -         setup_thy_loader ();
    2.37 -         setup_present_hook ();
    2.38 -         initialized := true);
    2.39 -       sync_thy_loader ();
    2.40 -       Unsynchronized.change print_mode (update (op =) ProofGeneralPgip.proof_general_emacsN);
    2.41 -       Secure.PG_setup ();
    2.42 -       Isar.toplevel_loop TextIO.stdIn
    2.43 -        {init = true, welcome = true, sync = true, secure = Secure.is_secure ()});
    2.44 +fun init () =
    2.45 +  (if ! initialized then ()
    2.46 +   else
    2.47 +    (Output.add_mode Symbol.xsymbolsN Symbol.output Output.default_escape;
    2.48 +     Output.add_mode ProofGeneralPgip.proof_general_emacsN
    2.49 +      Output.default_output Output.default_escape;
    2.50 +     Markup.add_mode ProofGeneralPgip.proof_general_emacsN YXML.output_markup;
    2.51 +     setup_messages ();
    2.52 +     ProofGeneralPgip.init_pgip_session_id ();
    2.53 +     setup_thy_loader ();
    2.54 +     setup_present_hook ();
    2.55 +     initialized := true);
    2.56 +   sync_thy_loader ();
    2.57 +   Unsynchronized.change print_mode (update (op =) ProofGeneralPgip.proof_general_emacsN);
    2.58 +   Secure.PG_setup ();
    2.59 +   Isar.toplevel_loop TextIO.stdIn
    2.60 +    {init = true, welcome = true, sync = true, secure = Secure.is_secure ()});
    2.61  
    2.62  
    2.63  (* fake old ThyLoad -- with new semantics *)