# HG changeset patch # User wenzelm # Date 1414750697 -3600 # Node ID 22b87ab47d3b45116415142f8ca7e17914a7fc06 # Parent f4bb3068d819f12a719074e7466e4b713e4a23a1 discontinued Proof General; diff -r f4bb3068d819 -r 22b87ab47d3b Admin/ProofGeneral/3.7.1.1/interface --- a/Admin/ProofGeneral/3.7.1.1/interface Thu Oct 30 23:14:11 2014 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,262 +0,0 @@ -#!/usr/bin/env bash -# -# interface,v 9.1 2008/02/06 15:40:45 makarius Exp -# -# Proof General interface wrapper for Isabelle. - - -## self references - -THIS="$(cd "$(dirname "$0")"; pwd)" -SUPER="$(cd "$THIS/.."; pwd)" - - -## diagnostics - -usage() -{ - echo - echo "Usage: Isabelle [OPTIONS] [FILES ...]" - echo - echo " Options are:" - echo " -I BOOL use Isabelle/Isar (default: true, implied by -P true)" - echo " -L NAME abbreviates -l NAME -k NAME" - echo " -P BOOL actually start Proof General (default true), otherwise" - echo " run plain tty session" - echo " -U BOOL enable Unicode (UTF-8) communication (default true)" - echo " -X BOOL configure the X-Symbol package on startup (default true)" - echo " -f SIZE set X-Symbol font size (default 12)" - echo " -g GEOMETRY specify Emacs geometry" - echo " -k NAME use specific isar-keywords for named logic" - echo " -l NAME logic image name (default \$ISABELLE_LOGIC=$ISABELLE_LOGIC)" - echo " -m MODE add print mode for output" - echo " -p NAME Emacs program name (default emacs)" - echo " -u BOOL use personal .emacs file (default true)" - echo " -w BOOL use window system (default true)" - echo " -x BOOL enable the X-Symbol package on startup (default false)" - echo - echo "Starts Proof General for Isabelle with theory and proof FILES" - echo "(default Scratch.thy)." - echo - echo " PROOFGENERAL_OPTIONS=$PROOFGENERAL_OPTIONS" - echo - exit 1 -} - -fail() -{ - echo "$1" >&2 - exit 2 -} - - -## process command line - -# options - -ISABELLE_OPTIONS="" -ISAR="true" -START_PG="true" -GEOMETRY="" -KEYWORDS="" -LOGIC="$ISABELLE_LOGIC" -PROGNAME="emacs" -INITFILE="true" -WINDOWSYSTEM="true" -XSYMBOL="" -XSYMBOL_SETUP=true -XSYMBOL_FONTSIZE="12" -UNICODE="" - -getoptions() -{ - OPTIND=1 - while getopts "I:L:P:U:X:f:g:k:l:m:p:u:w:x:" OPT - do - case "$OPT" in - I) - ISAR="$OPTARG" - ;; - L) - KEYWORDS="$OPTARG" - LOGIC="$OPTARG" - ;; - P) - START_PG="$OPTARG" - ;; - U) - UNICODE="$OPTARG" - ;; - X) - XSYMBOL_SETUP="$OPTARG" - ;; - f) - XSYMBOL_FONTSIZE="$OPTARG" - ;; - g) - GEOMETRY="$OPTARG" - ;; - k) - KEYWORDS="$OPTARG" - ;; - l) - LOGIC="$OPTARG" - ;; - m) - if [ -z "$ISABELLE_OPTIONS" ]; then - ISABELLE_OPTIONS="-m $OPTARG" - else - ISABELLE_OPTIONS="$ISABELLE_OPTIONS -m $OPTARG" - fi - ;; - p) - PROGNAME="$OPTARG" - ;; - u) - INITFILE="$OPTARG" - ;; - w) - WINDOWSYSTEM="$OPTARG" - ;; - x) - XSYMBOL="$OPTARG" - ;; - \?) - usage - ;; - esac - done -} - -eval "OPTIONS=($PROOFGENERAL_OPTIONS)" -getoptions "${OPTIONS[@]}" - -getoptions "$@" -shift $(($OPTIND - 1)) - - -# args - -declare -a FILES=() - -if [ "$#" -eq 0 ]; then - FILES["${#FILES[@]}"]="Scratch.thy" -else - while [ "$#" -gt 0 ]; do - FILES["${#FILES[@]}"]="$1" - shift - done -fi - - -## smart X11 font installation - -function checkfonts () -{ - XLSFONTS=$(xlsfonts -fn "-xsymb-xsymb0-*" 2>&1) || return 1 - - case "$XLSFONTS" in - xlsfonts:*) - return 1 - ;; - esac - - return 0 -} - -function installfonts () -{ - checkfonts "$XSYMBOL_PATTERN" || eval $XSYMBOL_INSTALLFONTS -} - - -## main - -# Isabelle2008 compatibility -[ -z "$ISABELLE_PROCESS" ] && export ISABELLE_PROCESS="$ISABELLE" -[ -z "$ISABELLE_TOOL" ] && export ISABELLE_TOOL="$ISATOOL" - -if [ "$START_PG" = false ]; then - - [ "$ISAR" = true ] && ISABELLE_OPTIONS="$ISABELLE_OPTIONS -I" - exec "$ISABELLE_PROCESS" $ISABELLE_OPTIONS "$LOGIC" - -else - - declare -a ARGS=() - - if [ -n "$GEOMETRY" ]; then - ARGS["${#ARGS[@]}"]="-geometry" - ARGS["${#ARGS[@]}"]="$GEOMETRY" - fi - - [ "$INITFILE" = false ] && ARGS["${#ARGS[@]}"]="-q" - - if [ "$WINDOWSYSTEM" = false ]; then - ARGS["${#ARGS[@]}"]="-nw" - XSYMBOL=false - elif [ -z "$DISPLAY" ]; then - XSYMBOL=false - else - [ -n "$XSYMBOL_INSTALLFONTS" -a "$XSYMBOL_SETUP" = true ] && installfonts - fi - - if [ $(uname -s) = Darwin -a -d "$HOME/Library/Fonts" ] - then - if [ ! -f "$HOME/Library/Fonts/XSymb0Medium.ttf" -o ! -f "$HOME/Library/Fonts/XSymb1Medium.ttf" ] - then - cp -f "$SUPER/x-symbol/etc/fonts-ttf/XSymb0Medium.ttf" "$HOME/Library/Fonts/" - cp -f "$SUPER/x-symbol/etc/fonts-ttf/XSymb1Medium.ttf" "$HOME/Library/Fonts/" - sleep 3 - fi - fi - - ARGS["${#ARGS[@]}"]="-l" - ARGS["${#ARGS[@]}"]="$SUPER/isar/interface-setup.el" - - if [ -n "$KEYWORDS" ]; then - if [ -f "$ISABELLE_HOME_USER/etc/isar-keywords-$KEYWORDS.el" ]; then - ARGS["${#ARGS[@]}"]="-l" - ARGS["${#ARGS[@]}"]="$ISABELLE_HOME_USER/etc/isar-keywords-$KEYWORDS.el" - elif [ -f "$ISABELLE_HOME/etc/isar-keywords-$KEYWORDS.el" ]; then - ARGS["${#ARGS[@]}"]="-l" - ARGS["${#ARGS[@]}"]="$ISABELLE_HOME/etc/isar-keywords-$KEYWORDS.el" - else - fail "No isar-keywords file for '$KEYWORDS'" - fi - elif [ -f "$ISABELLE_HOME_USER/etc/isar-keywords.el" ]; then - ARGS["${#ARGS[@]}"]="-l" - ARGS["${#ARGS[@]}"]="$ISABELLE_HOME_USER/etc/isar-keywords.el" - elif [ -f "$ISABELLE_HOME/etc/isar-keywords.el" ]; then - ARGS["${#ARGS[@]}"]="-l" - ARGS["${#ARGS[@]}"]="$ISABELLE_HOME/etc/isar-keywords.el" - fi - - for FILE in "$ISABELLE_HOME/etc/proofgeneral-settings.el" \ - "$ISABELLE_HOME_USER/etc/proofgeneral-settings.el" - do - if [ -f "$FILE" ]; then - ARGS["${#ARGS[@]}"]="-l" - ARGS["${#ARGS[@]}"]="$FILE" - fi - done - - case "$LOGIC" in - /*) - ;; - */*) - LOGIC="$(pwd -P)/$LOGIC" - ;; - esac - - export PROOFGENERAL_HOME="$SUPER" - export PROOFGENERAL_ASSISTANTS="isar" - export PROOFGENERAL_LOGIC="$LOGIC" - export PROOFGENERAL_XSYMBOL="$XSYMBOL" - export PROOFGENERAL_UNICODE="$UNICODE" - - export ISABELLE_OPTIONS XSYMBOL_FONTSIZE - - exec "$PROGNAME" "${ARGS[@]}" "${FILES[@]}" - -fi diff -r f4bb3068d819 -r 22b87ab47d3b Admin/ProofGeneral/3.7.1.1/isar-antiq-regexp.patch --- a/Admin/ProofGeneral/3.7.1.1/isar-antiq-regexp.patch Thu Oct 30 23:14:11 2014 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,21 +0,0 @@ ---- a/isar/isar-syntax.el Wed Aug 06 11:43:47 2008 +0200 -+++ b/isar/isar-syntax.el Thu Sep 18 15:21:16 2008 +0200 -@@ -252,14 +252,9 @@ - - ;; antiquotations - --;; the \{0,10\} bound is there because otherwise font-lock sometimes hangs for --;; incomplete antiquotations like @{text bla"} (even though it is supposed to --;; stop at eol anyway). -- --(defconst isar-antiq-regexp -- (concat "@{\\(?:[^\"{}]+\\|" isar-string "\\)\\{0,10\\}}") -- "Regexp matching Isabelle/Isar antiquoations.") -- -+(defconst isar-antiq-regexp -+ (concat "@{\\(?:[^\"{}]\\|" isar-string "\\)*}") -+ "Regexp matching Isabelle/Isar antiquotations.") - - ;; keyword nesting - - diff -r f4bb3068d819 -r 22b87ab47d3b Admin/ProofGeneral/3.7.1.1/menu.patch --- a/Admin/ProofGeneral/3.7.1.1/menu.patch Thu Oct 30 23:14:11 2014 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,30 +0,0 @@ ---- a/isar/isar.el 2008-07-10 20:47:49.000000000 +0200 -+++ b/isar/isar.el 2009-11-26 20:51:44.103016094 +0100 -@@ -339,9 +339,12 @@ - (error "Aborted.")) - [(control p)]) - --(proof-definvisible isar-cmd-refute "refute" [r]) - (proof-definvisible isar-cmd-quickcheck "quickcheck" [(control q)]) -+(proof-definvisible isar-cmd-nitpick "nitpick" [(control n)]) -+(proof-definvisible isar-cmd-refute "refute" [r]) - (proof-definvisible isar-cmd-sledgehammer "sledgehammer" [(control s)]) -+(proof-definvisible isar-cmd-atp-kill "atp_kill") -+(proof-definvisible isar-cmd-atp-info "atp_info") - - (defpgdefault menu-entries - (append -@@ -349,9 +352,12 @@ - (list - (cons "Commands" - (list -- ["refute" isar-cmd-refute t] - ["quickcheck" isar-cmd-quickcheck t] -+ ["nitpick" isar-cmd-nitpick t] -+ ["refute" isar-cmd-refute t] - ["sledgehammer" isar-cmd-sledgehammer t] -+ ["sledgehammer: kill" isar-cmd-atp-kill t] -+ ["sledgehammer: info" isar-cmd-atp-info t] - ["display draft" isar-cmd-display-draft t]))) - (list - (cons "Show me ..." diff -r f4bb3068d819 -r 22b87ab47d3b Admin/ProofGeneral/3.7.1.1/progname.patch --- a/Admin/ProofGeneral/3.7.1.1/progname.patch Thu Oct 30 23:14:11 2014 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,89 +0,0 @@ ---- a/isar/isabelle-system.el 2008-07-17 00:37:36.000000000 +0200 -+++ b/isar/isabelle-system.el 2009-11-30 17:06:05.508481278 +0100 -@@ -97,8 +97,8 @@ - (if (or proof-rsh-command - (file-executable-p isa-isatool-command)) - (let ((setting (isa-shell-command-to-string -- (concat isa-isatool-command -- " getenv -b " envvar)))) -+ (concat "\"" isa-isatool-command -+ "\" getenv -b " envvar)))) - (if (string-equal setting "") - default - setting)) -@@ -125,15 +125,12 @@ - :type 'file - :group 'isabelle) - --(defvar isabelle-prog-name nil -- "Set from `isabelle-set-prog-name', has name of logic appended sometimes.") -- - (defun isa-tool-list-logics () - "Generate a list of available object logics." - (if (isa-set-isatool-command) - (delete "" (split-string - (isa-shell-command-to-string -- (concat isa-isatool-command " findlogics")) "[ \t]")))) -+ (concat "\"" isa-isatool-command "\" findlogics")) "[ \t]")))) - - (defcustom isabelle-logics-available nil - "*List of logics available to use with Isabelle. -@@ -177,7 +174,7 @@ - - (defun isabelle-set-prog-name (&optional filename) - "Make proper command line for running Isabelle. --This function sets `isabelle-prog-name' and `proof-prog-name'." -+This function sets `proof-prog-name' and `isar-prog-args'." - (let* - ;; The ISABELLE and PROOFGENERAL_LOGIC values (set when run - ;; under the interface wrapper script) indicate command line -@@ -187,21 +184,20 @@ - (getenv "ISABELLE") ; command line override - (isa-getenv "ISABELLE") ; choose to match isatool - "isabelle")) ; to -- (isabelle-opts (getenv "ISABELLE_OPTIONS")) -- (opts (concat " -PI" ;; Proof General + Isar -- (if proof-shell-unicode " -m PGASCII" "") -- (if (and isabelle-opts (not (equal isabelle-opts ""))) -- (concat " " isabelle-opts) ""))) -+ (isabelle-opts (split-string (getenv "ISABELLE_OPTIONS"))) -+ (opts (append (list "-PI") ;; Proof General + Isar -+ (if proof-shell-unicode (list "-m" "PGASCII") nil) -+ isabelle-opts)) - (logic (or isabelle-chosen-logic - (getenv "PROOFGENERAL_LOGIC"))) - (logicarg (if (and logic (not (equal logic ""))) -- (concat " " logic) ""))) -+ (list logic) nil))) - (setq isabelle-chosen-logic-prev isabelle-chosen-logic) -- (setq isabelle-prog-name (concat isabelle opts logicarg)) -- (setq proof-prog-name isabelle-prog-name))) -+ (setq isar-prog-args (append opts logicarg)) -+ (setq proof-prog-name isabelle))) - - (defun isabelle-choose-logic (logic) -- "Adjust isabelle-prog-name and proof-prog-name for running LOGIC." -+ "Adjust proof-prog-name and isar-prog-args for running LOGIC." - (interactive - (list (completing-read - "Use logic: " -@@ -224,9 +220,7 @@ - (if (isa-set-isatool-command) - (apply 'start-process - "isa-view-doc" nil -- (append (split-string -- isa-isatool-command) -- (list "doc" docname))))) -+ (list isa-isatool-command "doc" docname)))) - - (defun isa-tool-list-docs () - "Generate a list of documentation files available, with descriptions. -@@ -236,7 +230,7 @@ - passed to isa-tool-doc-command, DOCNAME will be viewed." - (if (isa-set-isatool-command) - (let ((docs (isa-shell-command-to-string -- (concat isa-isatool-command " doc")))) -+ (concat "\"" isa-isatool-command "\" doc")))) - (unless (string-equal docs "") - (mapcan - (function (lambda (docdes) diff -r f4bb3068d819 -r 22b87ab47d3b Admin/ProofGeneral/3.7.1.1/timeout.patch --- a/Admin/ProofGeneral/3.7.1.1/timeout.patch Thu Oct 30 23:14:11 2014 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,11 +0,0 @@ ---- a/generic/proof-config.el 2008-07-21 18:37:10.000000000 +0200 -+++ b/generic/proof-config.el 2009-11-29 17:41:37.409062091 +0100 -@@ -1493,7 +1493,7 @@ - :type '(choice string (const nil)) - :group 'proof-shell) - --(defcustom proof-shell-quit-timeout 4 -+(defcustom proof-shell-quit-timeout 45 - ;; FIXME could add option to quiz user before rude kill. - "The number of seconds to wait after sending proof-shell-quit-cmd. - After this timeout, the proof shell will be killed off more rudely. diff -r f4bb3068d819 -r 22b87ab47d3b Admin/ProofGeneral/3.7.1.1/version.patch --- a/Admin/ProofGeneral/3.7.1.1/version.patch Thu Oct 30 23:14:11 2014 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,20 +0,0 @@ ---- a/generic/proof-site.el 2008-07-23 14:40:14.000000000 +0200 -+++ b/generic/proof-site.el 2009-11-28 16:13:56.409505412 +0100 -@@ -55,7 +55,7 @@ - - (eval-and-compile - ;; WARNING: do not edit next line (constant is edited in Makefile.devel) -- (defconst proof-general-version "Proof General Version 3.7.1. Released by da on Wed 23 Jul 2008." -+ (defconst proof-general-version "Proof General Version 3.7.1.1. Fabricated by makarius on Mon 30 Nov 2009." - "Version string identifying Proof General release.")) - - (defconst proof-general-short-version -@@ -64,7 +64,7 @@ - (string-match "Version \\([^ ]+\\)\\." proof-general-version) - (match-string 1 proof-general-version)))) - --(defconst proof-general-version-year "2008") -+(defconst proof-general-version-year "2009") - - ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; - ;; diff -r f4bb3068d819 -r 22b87ab47d3b Admin/components/optional --- a/Admin/components/optional Thu Oct 30 23:14:11 2014 +0100 +++ b/Admin/components/optional Fri Oct 31 11:18:17 2014 +0100 @@ -1,3 +1,2 @@ #optional components that could impact build time significantly hol-light-bundle-0.5-126 -ProofGeneral-4.2-2 diff -r f4bb3068d819 -r 22b87ab47d3b Admin/lib/Tools/update_keywords --- a/Admin/lib/Tools/update_keywords Thu Oct 30 23:14:11 2014 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,15 +0,0 @@ -#!/usr/bin/env bash -# -# Author: Makarius -# -# DESCRIPTION: update standard keyword files for Emacs Proof General -# (Proof General legacy) - -isabelle_admin_build jars || exit $? - -declare -a JAVA_ARGS; eval "JAVA_ARGS=($ISABELLE_BUILD_JAVA_OPTIONS)" - -cd "$ISABELLE_HOME/etc" - -"$ISABELLE_TOOL" java "${JAVA_ARGS[@]}" isabelle.Keywords update_keywords - diff -r f4bb3068d819 -r 22b87ab47d3b NEWS --- a/NEWS Thu Oct 30 23:14:11 2014 +0100 +++ b/NEWS Fri Oct 31 11:18:17 2014 +0100 @@ -187,6 +187,8 @@ *** System *** +* Proof General support has been discontinued. Minor INCOMPATIBILITY. + * The Isabelle tool "update_cartouches" changes theory files to use cartouches instead of old-style {* verbatim *} or `alt_string` tokens. diff -r f4bb3068d819 -r 22b87ab47d3b bin/isabelle_process --- a/bin/isabelle_process Thu Oct 30 23:14:11 2014 +0100 +++ b/bin/isabelle_process Fri Oct 31 11:18:17 2014 +0100 @@ -28,7 +28,6 @@ echo " Options are:" echo " -I startup Isar interaction mode" echo " -O system options from given YXML file" - echo " -P startup Proof General interaction mode" echo " -S secure mode -- disallow critical operations" echo " -T ADDR startup process wrapper, with socket address" echo " -W IN:OUT startup process wrapper, with input/output fifos" @@ -60,7 +59,6 @@ ISAR="" OPTIONS_FILE="" -PROOFGENERAL="" SECURE="" WRAPPER_SOCKET="" WRAPPER_FIFOS="" @@ -71,7 +69,7 @@ READONLY="" NOWRITE="" -while getopts "IO:PST:W:e:m:o:qrw" OPT +while getopts "IO:ST:W:e:m:o:qrw" OPT do case "$OPT" in I) @@ -80,9 +78,6 @@ O) OPTIONS_FILE="$OPTARG" ;; - P) - PROOFGENERAL=true - ;; S) SECURE=true ;; @@ -237,9 +232,7 @@ if [ "$INPUT" != RAW_ML_SYSTEM -a "$INPUT" != RAW ]; then MLTEXT="Exn.capture_exit 2 Options.load_default (); $MLTEXT" fi - if [ -n "$PROOFGENERAL" ]; then - MLTEXT="$MLTEXT; ProofGeneral.init ();" - elif [ -n "$ISAR" ]; then + if [ -n "$ISAR" ]; then MLTEXT="$MLTEXT; Isar.main ();" else NICE="" diff -r f4bb3068d819 -r 22b87ab47d3b etc/isar-keywords-ZF.el --- a/etc/isar-keywords-ZF.el Thu Oct 30 23:14:11 2014 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,502 +0,0 @@ -;; -;; Keyword classification tables for Isabelle/Isar. -;; Generated from Pure + ZF. -;; *** DO NOT EDIT *** DO NOT EDIT *** DO NOT EDIT *** -;; - -(defconst isar-keywords-major - '("\\." - "\\.\\." - "Isabelle\\.command" - "ML" - "ML_command" - "ML_file" - "ML_prf" - "ML_val" - "ProofGeneral\\.inform_file_processed" - "ProofGeneral\\.inform_file_retracted" - "ProofGeneral\\.kill_proof" - "ProofGeneral\\.pr" - "ProofGeneral\\.process_pgip" - "ProofGeneral\\.restart" - "ProofGeneral\\.undo" - "SML_export" - "SML_file" - "SML_import" - "abbreviation" - "also" - "apply" - "apply_end" - "assume" - "attribute_setup" - "axiomatization" - "back" - "bundle" - "by" - "cannot_undo" - "case" - "chapter" - "class" - "class_deps" - "codatatype" - "code_datatype" - "coinductive" - "commit" - "consts" - "context" - "corollary" - "datatype" - "declaration" - "declare" - "def" - "default_sort" - "defer" - "definition" - "defs" - "disable_pr" - "display_drafts" - "done" - "enable_pr" - "end" - "exit" - "extract" - "extract_type" - "finally" - "find_consts" - "find_theorems" - "fix" - "from" - "full_prf" - "guess" - "have" - "header" - "help" - "hence" - "hide_class" - "hide_const" - "hide_fact" - "hide_type" - "include" - "including" - "inductive" - "inductive_cases" - "init_toplevel" - "instance" - "instantiation" - "interpret" - "interpretation" - "judgment" - "kill" - "kill_thy" - "lemma" - "lemmas" - "let" - "linear_undo" - "local_setup" - "locale" - "locale_deps" - "method_setup" - "moreover" - "named_theorems" - "next" - "no_notation" - "no_syntax" - "no_translations" - "no_type_notation" - "nonterminal" - "notation" - "note" - "notepad" - "obtain" - "oops" - "oracle" - "overloading" - "parse_ast_translation" - "parse_translation" - "pr" - "prefer" - "presume" - "pretty_setmargin" - "prf" - "primrec" - "print_ML_antiquotations" - "print_abbrevs" - "print_antiquotations" - "print_ast_translation" - "print_attributes" - "print_binds" - "print_bundles" - "print_cases" - "print_claset" - "print_classes" - "print_codesetup" - "print_commands" - "print_context" - "print_defn_rules" - "print_dependencies" - "print_facts" - "print_induct_rules" - "print_interps" - "print_locale" - "print_locales" - "print_methods" - "print_options" - "print_rules" - "print_simpset" - "print_state" - "print_statement" - "print_syntax" - "print_tcset" - "print_term_bindings" - "print_theorems" - "print_theory" - "print_trans_rules" - "print_translation" - "proof" - "prop" - "qed" - "quit" - "realizability" - "realizers" - "remove_thy" - "rep_datatype" - "schematic_corollary" - "schematic_lemma" - "schematic_theorem" - "sect" - "section" - "setup" - "show" - "simproc_setup" - "sorry" - "subclass" - "sublocale" - "subsect" - "subsection" - "subsubsect" - "subsubsection" - "syntax" - "syntax_declaration" - "term" - "text" - "text_raw" - "then" - "theorem" - "theorems" - "theory" - "thm" - "thm_deps" - "thus" - "thy_deps" - "translations" - "txt" - "txt_raw" - "typ" - "type_notation" - "type_synonym" - "typed_print_translation" - "typedecl" - "ultimately" - "undo" - "undos_proof" - "unfolding" - "unused_thms" - "use_thy" - "using" - "welcome" - "with" - "write" - "{" - "}")) - -(defconst isar-keywords-minor - '("and" - "assumes" - "attach" - "begin" - "binder" - "case_eqns" - "con_defs" - "constrains" - "defines" - "domains" - "elimination" - "fixes" - "for" - "identifier" - "if" - "imports" - "in" - "includes" - "induction" - "infix" - "infixl" - "infixr" - "intros" - "is" - "keywords" - "monos" - "notes" - "obtains" - "open" - "output" - "overloaded" - "pervasive" - "recursor_eqns" - "shows" - "structure" - "type_elims" - "type_intros" - "unchecked" - "where")) - -(defconst isar-keywords-control - '("Isabelle\\.command" - "ProofGeneral\\.inform_file_processed" - "ProofGeneral\\.inform_file_retracted" - "ProofGeneral\\.kill_proof" - "ProofGeneral\\.pr" - "ProofGeneral\\.process_pgip" - "ProofGeneral\\.restart" - "ProofGeneral\\.undo" - "cannot_undo" - "commit" - "disable_pr" - "enable_pr" - "exit" - "init_toplevel" - "kill" - "kill_thy" - "linear_undo" - "pretty_setmargin" - "quit" - "remove_thy" - "undo" - "undos_proof" - "use_thy")) - -(defconst isar-keywords-diag - '("ML_command" - "ML_val" - "class_deps" - "display_drafts" - "find_consts" - "find_theorems" - "full_prf" - "header" - "help" - "locale_deps" - "pr" - "prf" - "print_ML_antiquotations" - "print_abbrevs" - "print_antiquotations" - "print_attributes" - "print_binds" - "print_bundles" - "print_cases" - "print_claset" - "print_classes" - "print_codesetup" - "print_commands" - "print_context" - "print_defn_rules" - "print_dependencies" - "print_facts" - "print_induct_rules" - "print_interps" - "print_locale" - "print_locales" - "print_methods" - "print_options" - "print_rules" - "print_simpset" - "print_state" - "print_statement" - "print_syntax" - "print_tcset" - "print_term_bindings" - "print_theorems" - "print_theory" - "print_trans_rules" - "prop" - "term" - "thm" - "thm_deps" - "thy_deps" - "typ" - "unused_thms" - "welcome")) - -(defconst isar-keywords-theory-begin - '("theory")) - -(defconst isar-keywords-theory-switch - '()) - -(defconst isar-keywords-theory-end - '("end")) - -(defconst isar-keywords-theory-heading - '("chapter" - "section" - "subsection" - "subsubsection")) - -(defconst isar-keywords-theory-decl - '("ML" - "ML_file" - "SML_export" - "SML_file" - "SML_import" - "abbreviation" - "attribute_setup" - "axiomatization" - "bundle" - "class" - "codatatype" - "code_datatype" - "coinductive" - "consts" - "context" - "datatype" - "declaration" - "declare" - "default_sort" - "definition" - "defs" - "extract" - "extract_type" - "hide_class" - "hide_const" - "hide_fact" - "hide_type" - "inductive" - "inductive_cases" - "instantiation" - "judgment" - "lemmas" - "local_setup" - "locale" - "method_setup" - "named_theorems" - "no_notation" - "no_syntax" - "no_translations" - "no_type_notation" - "nonterminal" - "notation" - "notepad" - "oracle" - "overloading" - "parse_ast_translation" - "parse_translation" - "primrec" - "print_ast_translation" - "print_translation" - "realizability" - "realizers" - "rep_datatype" - "setup" - "simproc_setup" - "syntax" - "syntax_declaration" - "text" - "text_raw" - "theorems" - "translations" - "type_notation" - "type_synonym" - "typed_print_translation" - "typedecl")) - -(defconst isar-keywords-theory-script - '()) - -(defconst isar-keywords-theory-goal - '("corollary" - "instance" - "interpretation" - "lemma" - "schematic_corollary" - "schematic_lemma" - "schematic_theorem" - "subclass" - "sublocale" - "theorem")) - -(defconst isar-keywords-qed - '("\\." - "\\.\\." - "by" - "done" - "sorry")) - -(defconst isar-keywords-qed-block - '("qed")) - -(defconst isar-keywords-qed-global - '("oops")) - -(defconst isar-keywords-proof-heading - '("sect" - "subsect" - "subsubsect")) - -(defconst isar-keywords-proof-goal - '("have" - "hence" - "interpret")) - -(defconst isar-keywords-proof-block - '("next" - "proof")) - -(defconst isar-keywords-proof-open - '("{")) - -(defconst isar-keywords-proof-close - '("}")) - -(defconst isar-keywords-proof-chain - '("finally" - "from" - "then" - "ultimately" - "with")) - -(defconst isar-keywords-proof-decl - '("ML_prf" - "also" - "include" - "including" - "let" - "moreover" - "note" - "txt" - "txt_raw" - "unfolding" - "using" - "write")) - -(defconst isar-keywords-proof-asm - '("assume" - "case" - "def" - "fix" - "presume")) - -(defconst isar-keywords-proof-asm-goal - '("guess" - "obtain" - "show" - "thus")) - -(defconst isar-keywords-proof-script - '("apply" - "apply_end" - "back" - "defer" - "prefer")) - -(provide 'isar-keywords) diff -r f4bb3068d819 -r 22b87ab47d3b etc/isar-keywords.el --- a/etc/isar-keywords.el Thu Oct 30 23:14:11 2014 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,718 +0,0 @@ -;; -;; Keyword classification tables for Isabelle/Isar. -;; Generated from HOL + HOL-Auth + HOL-Bali + HOL-Datatype_Examples + HOL-Decision_Procs + HOL-Hahn_Banach + HOL-IMP + HOL-Imperative_HOL + HOL-Import + HOL-Induct + HOL-Library + HOL-Multivariate_Analysis + HOL-Mutabelle + HOL-Nominal + HOL-Predicate_Compile_Examples + HOL-Probability + HOL-Proofs + HOL-Proofs-Extraction + HOL-SPARK + HOL-Statespace + HOL-TPTP + HOL-Word-SMT_Examples + HOL-ex + HOLCF + Pure. -;; *** DO NOT EDIT *** DO NOT EDIT *** DO NOT EDIT *** -;; - -(defconst isar-keywords-major - '("\\." - "\\.\\." - "Isabelle\\.command" - "ML" - "ML_command" - "ML_file" - "ML_prf" - "ML_val" - "ProofGeneral\\.inform_file_processed" - "ProofGeneral\\.inform_file_retracted" - "ProofGeneral\\.kill_proof" - "ProofGeneral\\.pr" - "ProofGeneral\\.process_pgip" - "ProofGeneral\\.restart" - "ProofGeneral\\.undo" - "SML_export" - "SML_file" - "SML_import" - "abbreviation" - "adhoc_overloading" - "also" - "apply" - "apply_end" - "approximate" - "assume" - "atom_decl" - "attribute_setup" - "axiomatization" - "back" - "bnf" - "bnf_axiomatization" - "boogie_file" - "bundle" - "by" - "cannot_undo" - "cartouche" - "case" - "case_of_simps" - "chapter" - "class" - "class_deps" - "codatatype" - "code_datatype" - "code_deps" - "code_identifier" - "code_monad" - "code_pred" - "code_printing" - "code_reflect" - "code_reserved" - "code_thms" - "coinductive" - "coinductive_set" - "commit" - "consts" - "context" - "corollary" - "cpodef" - "datatype" - "datatype_compat" - "declaration" - "declare" - "def" - "default_sort" - "defer" - "defer_recdef" - "definition" - "defs" - "disable_pr" - "display_drafts" - "domain" - "domain_isomorphism" - "domaindef" - "done" - "enable_pr" - "end" - "equivariance" - "exit" - "export_code" - "extract" - "extract_type" - "finally" - "find_consts" - "find_theorems" - "find_unused_assms" - "fix" - "fixrec" - "free_constructors" - "from" - "full_prf" - "fun" - "fun_cases" - "function" - "functor" - "guess" - "have" - "header" - "help" - "hence" - "hide_class" - "hide_const" - "hide_fact" - "hide_type" - "import_const_map" - "import_file" - "import_tptp" - "import_type_map" - "include" - "including" - "inductive" - "inductive_cases" - "inductive_set" - "inductive_simps" - "init_toplevel" - "instance" - "instantiation" - "interpret" - "interpretation" - "judgment" - "kill" - "kill_thy" - "lemma" - "lemmas" - "let" - "lift_definition" - "lifting_forget" - "lifting_update" - "linear_undo" - "local_setup" - "locale" - "locale_deps" - "method_setup" - "moreover" - "named_theorems" - "next" - "nitpick" - "nitpick_params" - "no_adhoc_overloading" - "no_notation" - "no_syntax" - "no_translations" - "no_type_notation" - "nominal_datatype" - "nominal_function" - "nominal_inductive" - "nominal_inductive2" - "nominal_primrec" - "nominal_termination" - "nonterminal" - "notation" - "note" - "notepad" - "obtain" - "old_datatype" - "old_rep_datatype" - "old_smt_status" - "oops" - "oracle" - "overloading" - "parse_ast_translation" - "parse_translation" - "partial_function" - "pcpodef" - "permanent_interpretation" - "pr" - "prefer" - "presume" - "pretty_setmargin" - "prf" - "primcorec" - "primcorecursive" - "primrec" - "print_ML_antiquotations" - "print_abbrevs" - "print_antiquotations" - "print_ast_translation" - "print_attributes" - "print_binds" - "print_bnfs" - "print_bundles" - "print_case_translations" - "print_cases" - "print_claset" - "print_classes" - "print_codeproc" - "print_codesetup" - "print_coercions" - "print_commands" - "print_context" - "print_defn_rules" - "print_dependencies" - "print_facts" - "print_induct_rules" - "print_inductives" - "print_interps" - "print_locale" - "print_locales" - "print_methods" - "print_options" - "print_orders" - "print_quot_maps" - "print_quotconsts" - "print_quotients" - "print_quotientsQ3" - "print_quotmapsQ3" - "print_rules" - "print_simpset" - "print_state" - "print_statement" - "print_syntax" - "print_term_bindings" - "print_theorems" - "print_theory" - "print_trans_rules" - "print_translation" - "proof" - "prop" - "qed" - "quickcheck" - "quickcheck_generator" - "quickcheck_params" - "quit" - "quotient_definition" - "quotient_type" - "realizability" - "realizers" - "recdef" - "recdef_tc" - "record" - "refute" - "refute_params" - "remove_thy" - "schematic_corollary" - "schematic_lemma" - "schematic_theorem" - "sect" - "section" - "setup" - "setup_lifting" - "show" - "simproc_setup" - "simps_of_case" - "sledgehammer" - "sledgehammer_params" - "smt_status" - "solve_direct" - "sorry" - "spark_end" - "spark_open" - "spark_open_vcg" - "spark_proof_functions" - "spark_status" - "spark_types" - "spark_vc" - "specification" - "statespace" - "subclass" - "sublocale" - "subsect" - "subsection" - "subsubsect" - "subsubsection" - "syntax" - "syntax_declaration" - "term" - "term_cartouche" - "termination" - "test_code" - "text" - "text_cartouche" - "text_raw" - "then" - "theorem" - "theorems" - "theory" - "thm" - "thm_deps" - "thus" - "thy_deps" - "translations" - "try" - "try0" - "txt" - "txt_raw" - "typ" - "type_notation" - "type_synonym" - "typed_print_translation" - "typedecl" - "typedef" - "ultimately" - "undo" - "undos_proof" - "unfolding" - "unused_thms" - "use_thy" - "using" - "value" - "values" - "values_prolog" - "welcome" - "with" - "write" - "{" - "}")) - -(defconst isar-keywords-minor - '("and" - "assumes" - "attach" - "avoids" - "begin" - "binder" - "binds" - "checking" - "class_instance" - "class_relation" - "code_module" - "congs" - "constant" - "constrains" - "datatypes" - "defines" - "defining" - "file" - "fixes" - "for" - "functions" - "hints" - "identifier" - "if" - "imports" - "in" - "includes" - "infix" - "infixl" - "infixr" - "is" - "keywords" - "lazy" - "module_name" - "monos" - "morphisms" - "notes" - "obtains" - "open" - "output" - "overloaded" - "parametric" - "permissive" - "pervasive" - "shows" - "structure" - "type_class" - "type_constructor" - "unchecked" - "unsafe" - "where")) - -(defconst isar-keywords-control - '("Isabelle\\.command" - "ProofGeneral\\.inform_file_processed" - "ProofGeneral\\.inform_file_retracted" - "ProofGeneral\\.kill_proof" - "ProofGeneral\\.pr" - "ProofGeneral\\.process_pgip" - "ProofGeneral\\.restart" - "ProofGeneral\\.undo" - "cannot_undo" - "commit" - "disable_pr" - "enable_pr" - "exit" - "init_toplevel" - "kill" - "kill_thy" - "linear_undo" - "pretty_setmargin" - "quit" - "remove_thy" - "undo" - "undos_proof" - "use_thy")) - -(defconst isar-keywords-diag - '("ML_command" - "ML_val" - "approximate" - "cartouche" - "class_deps" - "code_deps" - "code_thms" - "display_drafts" - "find_consts" - "find_theorems" - "find_unused_assms" - "full_prf" - "header" - "help" - "locale_deps" - "nitpick" - "old_smt_status" - "pr" - "prf" - "print_ML_antiquotations" - "print_abbrevs" - "print_antiquotations" - "print_attributes" - "print_binds" - "print_bnfs" - "print_bundles" - "print_case_translations" - "print_cases" - "print_claset" - "print_classes" - "print_codeproc" - "print_codesetup" - "print_coercions" - "print_commands" - "print_context" - "print_defn_rules" - "print_dependencies" - "print_facts" - "print_induct_rules" - "print_inductives" - "print_interps" - "print_locale" - "print_locales" - "print_methods" - "print_options" - "print_orders" - "print_quot_maps" - "print_quotconsts" - "print_quotients" - "print_quotientsQ3" - "print_quotmapsQ3" - "print_rules" - "print_simpset" - "print_state" - "print_statement" - "print_syntax" - "print_term_bindings" - "print_theorems" - "print_theory" - "print_trans_rules" - "prop" - "quickcheck" - "refute" - "sledgehammer" - "smt_status" - "solve_direct" - "spark_status" - "term" - "term_cartouche" - "test_code" - "thm" - "thm_deps" - "thy_deps" - "try" - "try0" - "typ" - "unused_thms" - "value" - "values" - "values_prolog" - "welcome")) - -(defconst isar-keywords-theory-begin - '("theory")) - -(defconst isar-keywords-theory-switch - '()) - -(defconst isar-keywords-theory-end - '("end")) - -(defconst isar-keywords-theory-heading - '("chapter" - "section" - "subsection" - "subsubsection")) - -(defconst isar-keywords-theory-decl - '("ML" - "ML_file" - "SML_export" - "SML_file" - "SML_import" - "abbreviation" - "adhoc_overloading" - "atom_decl" - "attribute_setup" - "axiomatization" - "bnf_axiomatization" - "boogie_file" - "bundle" - "case_of_simps" - "class" - "codatatype" - "code_datatype" - "code_identifier" - "code_monad" - "code_printing" - "code_reflect" - "code_reserved" - "coinductive" - "coinductive_set" - "consts" - "context" - "datatype" - "datatype_compat" - "declaration" - "declare" - "default_sort" - "defer_recdef" - "definition" - "defs" - "domain" - "domain_isomorphism" - "domaindef" - "equivariance" - "export_code" - "extract" - "extract_type" - "fixrec" - "fun" - "fun_cases" - "hide_class" - "hide_const" - "hide_fact" - "hide_type" - "import_const_map" - "import_file" - "import_tptp" - "import_type_map" - "inductive" - "inductive_cases" - "inductive_set" - "inductive_simps" - "instantiation" - "judgment" - "lemmas" - "lifting_forget" - "lifting_update" - "local_setup" - "locale" - "method_setup" - "named_theorems" - "nitpick_params" - "no_adhoc_overloading" - "no_notation" - "no_syntax" - "no_translations" - "no_type_notation" - "nominal_datatype" - "nonterminal" - "notation" - "notepad" - "old_datatype" - "oracle" - "overloading" - "parse_ast_translation" - "parse_translation" - "partial_function" - "primcorec" - "primrec" - "print_ast_translation" - "print_translation" - "quickcheck_generator" - "quickcheck_params" - "realizability" - "realizers" - "recdef" - "record" - "refute_params" - "setup" - "setup_lifting" - "simproc_setup" - "simps_of_case" - "sledgehammer_params" - "spark_end" - "spark_open" - "spark_open_vcg" - "spark_proof_functions" - "spark_types" - "statespace" - "syntax" - "syntax_declaration" - "text" - "text_cartouche" - "text_raw" - "theorems" - "translations" - "type_notation" - "type_synonym" - "typed_print_translation" - "typedecl")) - -(defconst isar-keywords-theory-script - '()) - -(defconst isar-keywords-theory-goal - '("bnf" - "code_pred" - "corollary" - "cpodef" - "free_constructors" - "function" - "functor" - "instance" - "interpretation" - "lemma" - "lift_definition" - "nominal_function" - "nominal_inductive" - "nominal_inductive2" - "nominal_primrec" - "nominal_termination" - "old_rep_datatype" - "pcpodef" - "permanent_interpretation" - "primcorecursive" - "quotient_definition" - "quotient_type" - "recdef_tc" - "schematic_corollary" - "schematic_lemma" - "schematic_theorem" - "spark_vc" - "specification" - "subclass" - "sublocale" - "termination" - "theorem" - "typedef")) - -(defconst isar-keywords-qed - '("\\." - "\\.\\." - "by" - "done" - "sorry")) - -(defconst isar-keywords-qed-block - '("qed")) - -(defconst isar-keywords-qed-global - '("oops")) - -(defconst isar-keywords-proof-heading - '("sect" - "subsect" - "subsubsect")) - -(defconst isar-keywords-proof-goal - '("have" - "hence" - "interpret")) - -(defconst isar-keywords-proof-block - '("next" - "proof")) - -(defconst isar-keywords-proof-open - '("{")) - -(defconst isar-keywords-proof-close - '("}")) - -(defconst isar-keywords-proof-chain - '("finally" - "from" - "then" - "ultimately" - "with")) - -(defconst isar-keywords-proof-decl - '("ML_prf" - "also" - "include" - "including" - "let" - "moreover" - "note" - "txt" - "txt_raw" - "unfolding" - "using" - "write")) - -(defconst isar-keywords-proof-asm - '("assume" - "case" - "def" - "fix" - "presume")) - -(defconst isar-keywords-proof-asm-goal - '("guess" - "obtain" - "show" - "thus")) - -(defconst isar-keywords-proof-script - '("apply" - "apply_end" - "back" - "defer" - "prefer")) - -(provide 'isar-keywords) diff -r f4bb3068d819 -r 22b87ab47d3b lib/Tools/keywords --- a/lib/Tools/keywords Thu Oct 30 23:14:11 2014 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,60 +0,0 @@ -#!/usr/bin/env bash -# -# Author: Makarius -# -# DESCRIPTION: generate keyword files for Emacs Proof General - - -## diagnostics - -PRG="$(basename "$0")" - -function usage() -{ - echo - echo "Usage: isabelle $PRG [OPTIONS] [SESSIONS ...]" - echo - echo " Options are:" - echo " -d DIR include session directory" - echo " -k NAME specific name of keywords collection (default: empty)" - echo - echo " Generate keyword files for Emacs Proof General from Isabelle sessions." - echo - exit 1 -} - - -## process command line - -# options - -declare -a DIRS=() -KEYWORDS_NAME="" - -while getopts "d:k:" OPT -do - case "$OPT" in - d) - DIRS["${#DIRS[@]}"]="$OPTARG" - ;; - k) - KEYWORDS_NAME="$OPTARG" - ;; - \?) - usage - ;; - esac -done - -shift $(($OPTIND - 1)) - - -## main - -isabelle_admin_build jars || exit $? - -declare -a JAVA_ARGS; eval "JAVA_ARGS=($ISABELLE_BUILD_JAVA_OPTIONS)" - -"$ISABELLE_TOOL" java "${JAVA_ARGS[@]}" isabelle.Keywords keywords \ - "$KEYWORDS_NAME" "${DIRS[@]}" $'\n' "$@" - diff -r f4bb3068d819 -r 22b87ab47d3b src/Doc/Classes/Classes.thy --- a/src/Doc/Classes/Classes.thy Thu Oct 30 23:14:11 2014 +0100 +++ b/src/Doc/Classes/Classes.thy Fri Oct 31 11:18:17 2014 +0100 @@ -179,8 +179,7 @@ primrec declaration; by default, the local name of a class operation @{text f} to be instantiated on type constructor @{text \} is mangled as @{text f_\}. In case of uncertainty, these names may be - inspected using the @{command "print_context"} command or the - corresponding ProofGeneral button. + inspected using the @{command "print_context"} command. *} subsection {* Lifting and parametric types *} diff -r f4bb3068d819 -r 22b87ab47d3b src/Doc/Implementation/ML.thy --- a/src/Doc/Implementation/ML.thy Thu Oct 30 23:14:11 2014 +0100 +++ b/src/Doc/Implementation/ML.thy Fri Oct 31 11:18:17 2014 +0100 @@ -1056,9 +1056,7 @@ \begin{warn} The actual error channel is accessed via @{ML Output.error_message}, but - the old interaction protocol of Proof~General \emph{crashes} if that - function is used in regular ML code: error output and toplevel - command failure always need to coincide in classic TTY interaction. + this is normally not used directly in user code. \end{warn} \end{description} diff -r f4bb3068d819 -r 22b87ab47d3b src/Doc/Isar_Ref/Inner_Syntax.thy --- a/src/Doc/Isar_Ref/Inner_Syntax.thy Thu Oct 30 23:14:11 2014 +0100 +++ b/src/Doc/Isar_Ref/Inner_Syntax.thy Fri Oct 31 11:18:17 2014 +0100 @@ -151,8 +151,7 @@ and sort constraints. This enables Prover IDE users to retrieve that information via tooltips or popups while hovering with the mouse over the output window, for example. Consequently, this - option is enabled by default for Isabelle/jEdit, but disabled for - TTY and Proof~General~/Emacs where document markup would not work. + option is enabled by default for Isabelle/jEdit. \item @{attribute show_types} and @{attribute show_sorts} control printing of type constraints for term variables, and sort @@ -274,12 +273,6 @@ \end{description} - \begin{warn} - The old global reference @{ML print_mode} should never be used - directly in applications. Its main reason for being publicly - accessible is to support historic versions of Proof~General. - \end{warn} - \medskip The pretty printer for inner syntax maintains alternative mixfix productions for any print mode name invented by the user, say in commands like @{command notation} or @{command abbreviation}. @@ -299,9 +292,7 @@ \item @{verbatim xsymbols}: enable proper mathematical symbols instead of ASCII art.\footnote{This traditional mode name stems from - the ``X-Symbol'' package for old versions Proof~General with XEmacs, - although that package has been superseded by Unicode in recent - years.} + the ``X-Symbol'' package for classic Proof~General with XEmacs.} \item @{verbatim HTML}: additional mode that is active in HTML presentation of Isabelle theory sources; allows to provide diff -r f4bb3068d819 -r 22b87ab47d3b src/Doc/Isar_Ref/Outer_Syntax.thy --- a/src/Doc/Isar_Ref/Outer_Syntax.thy Thu Oct 30 23:14:11 2014 +0100 +++ b/src/Doc/Isar_Ref/Outer_Syntax.thy Fri Oct 31 11:18:17 2014 +0100 @@ -42,25 +42,10 @@ next command keyword. More advanced interfaces such as Isabelle/jEdit @{cite "Wenzel:2012"} - and Proof~General @{cite proofgeneral} do not require explicit - semicolons: command spans are determined by inspecting the content - of the editor buffer. In the printed presentation of Isabelle/Isar - documents semicolons are omitted altogether for readability. - - \begin{warn} - Proof~General requires certain syntax classification tables in - order to achieve properly synchronized interaction with the - Isabelle/Isar process. These tables need to be consistent with - the Isabelle version and particular logic image to be used in a - running session (common object-logics may well change the outer - syntax). The standard setup should work correctly with any of the - ``official'' logic images derived from Isabelle/HOL (including - HOLCF etc.). Users of alternative logics may need to tell - Proof~General explicitly, e.g.\ by giving an option @{verbatim "-k ZF"} - (in conjunction with @{verbatim "-l ZF"}, to specify the default - logic image). Note that option @{verbatim "-L"} does both - of this at the same time. - \end{warn} + do not require explicit semicolons: command spans are determined by + inspecting the content of the editor buffer. In the printed + presentation of Isabelle/Isar documents semicolons are omitted + altogether for readability. \ @@ -205,7 +190,7 @@ Common mathematical symbols such as @{text \} are represented in Isabelle as @{verbatim \}. There are infinitely many Isabelle symbols like this, although proper presentation is left to front-end - tools such as {\LaTeX}, Proof~General, or Isabelle/jEdit. A list of + tools such as {\LaTeX} or Isabelle/jEdit. A list of predefined Isabelle symbols that work well with these tools is given in \appref{app:symbols}. Note that @{verbatim "\"} does not belong to the @{text letter} category, since it is already used differently diff -r f4bb3068d819 -r 22b87ab47d3b src/Doc/System/Basics.thy --- a/src/Doc/System/Basics.thy Thu Oct 30 23:14:11 2014 +0100 +++ b/src/Doc/System/Basics.thy Fri Oct 31 11:18:17 2014 +0100 @@ -363,7 +363,6 @@ Options are: -I startup Isar interaction mode -O system options from given YXML file - -P startup Proof General interaction mode -S secure mode -- disallow critical operations -T ADDR startup process wrapper, with socket address -W IN:OUT startup process wrapper, with input/output fifos @@ -437,8 +436,6 @@ \medskip The @{verbatim "-I"} option makes Isabelle enter Isar interaction mode on startup, instead of the primitive ML top-level. - The @{verbatim "-P"} option configures the top-level loop for - interaction with the Proof General user interface. \medskip The @{verbatim "-T"} or @{verbatim "-W"} option makes Isabelle enter a special process wrapper for interaction via diff -r f4bb3068d819 -r 22b87ab47d3b src/Doc/Tutorial/Documents/Documents.thy --- a/src/Doc/Tutorial/Documents/Documents.thy Thu Oct 30 23:14:11 2014 +0100 +++ b/src/Doc/Tutorial/Documents/Documents.thy Fri Oct 31 11:18:17 2014 +0100 @@ -102,9 +102,8 @@ Here $ident$ is any sequence of letters. This results in an infinite store of symbols, whose interpretation is left to further front-end tools. For example, the - user-interface of Proof~General + X-Symbol and the Isabelle document - processor (see \S\ref{sec:document-preparation}) display the - \verb,\,\verb,, symbol as~@{text \}. + Isabelle document processor (see \S\ref{sec:document-preparation}) + display the \verb,\,\verb,, symbol as~@{text \}. A list of standard Isabelle symbols is given in @{cite "isabelle-isar-ref"}. You may introduce your own @@ -147,12 +146,7 @@ (*>*) text {* - \noindent Proof~General provides several input methods to enter - @{text \} in the text. If all fails one may just type a named - entity \verb,\,\verb,, by hand; the corresponding symbol will - be displayed after further input. - - More flexible is to provide alternative syntax forms + It is possible to provide alternative syntax forms through the \bfindex{print mode} concept~@{cite "isabelle-isar-ref"}. By convention, the mode of ``$xsymbols$'' is enabled whenever Proof~General's X-Symbol mode or {\LaTeX} output is active. Now diff -r f4bb3068d819 -r 22b87ab47d3b src/Doc/Tutorial/Types/Overloading.thy --- a/src/Doc/Tutorial/Types/Overloading.thy Thu Oct 30 23:14:11 2014 +0100 +++ b/src/Doc/Tutorial/Types/Overloading.thy Fri Oct 31 11:18:17 2014 +0100 @@ -37,8 +37,7 @@ suffix @{text "_nat"}; by default, the local name of a class operation @{text f} to be instantiated on type constructor @{text \} is mangled as @{text f_\}. In case of uncertainty, these names may be inspected -using the @{command "print_context"} command or the corresponding -ProofGeneral button. +using the @{command "print_context"} command. Although class @{class [source] plus} has no axioms, the instantiation must be formally concluded by a (trivial) instantiation proof ``..'': *} diff -r f4bb3068d819 -r 22b87ab47d3b src/HOL/ROOT --- a/src/HOL/ROOT Thu Oct 30 23:14:11 2014 +0100 +++ b/src/HOL/ROOT Fri Oct 31 11:18:17 2014 +0100 @@ -600,7 +600,6 @@ Simps_Case_Conv_Examples ML SAT_Examples - Nominal2_Dummy SOS SOS_Cert theories [skip_proofs = false] diff -r f4bb3068d819 -r 22b87ab47d3b src/HOL/Tools/Nitpick/nitpick_commands.ML --- a/src/HOL/Tools/Nitpick/nitpick_commands.ML Thu Oct 30 23:14:11 2014 +0100 +++ b/src/HOL/Tools/Nitpick/nitpick_commands.ML Fri Oct 31 11:18:17 2014 +0100 @@ -31,13 +31,6 @@ its time slot with several other automatic tools. *) val auto_try_max_scopes = 6 -val _ = - ProofGeneral.preference_option ProofGeneral.category_tracing - NONE - @{system_option auto_nitpick} - "auto-nitpick" - "Run Nitpick automatically" - type raw_param = string * string list val default_default_params = diff -r f4bb3068d819 -r 22b87ab47d3b src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML Thu Oct 30 23:14:11 2014 +0100 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML Fri Oct 31 11:18:17 2014 +0100 @@ -38,13 +38,6 @@ val running_learnersN = "running_learners" val refresh_tptpN = "refresh_tptp" -val _ = - ProofGeneral.preference_option ProofGeneral.category_tracing - NONE - @{system_option auto_sledgehammer} - "auto-sledgehammer" - "Run Sledgehammer automatically" - (** Sledgehammer commands **) fun add_fact_override ns : fact_override = {add = ns, del = [], only = false} @@ -58,20 +51,6 @@ val provers = Unsynchronized.ref "" -val _ = - ProofGeneral.preference_string ProofGeneral.category_proof - NONE - provers - "Sledgehammer: Provers" - "Default automatic provers (separated by whitespace)" - -val _ = - ProofGeneral.preference_option ProofGeneral.category_proof - NONE - @{system_option sledgehammer_timeout} - "Sledgehammer: Time Limit" - "ATPs will be interrupted after this time (in seconds)" - type raw_param = string * string list val default_default_params = diff -r f4bb3068d819 -r 22b87ab47d3b src/HOL/Tools/try0.ML --- a/src/HOL/Tools/try0.ML Thu Oct 30 23:14:11 2014 +0100 +++ b/src/HOL/Tools/try0.ML Fri Oct 31 11:18:17 2014 +0100 @@ -22,13 +22,6 @@ datatype mode = Auto_Try | Try | Normal; -val _ = - ProofGeneral.preference_option ProofGeneral.category_tracing - NONE - @{system_option auto_methods} - "auto-try0" - "Try standard proof methods"; - val default_timeout = seconds 5.0; fun can_apply timeout_opt pre post tac st = diff -r f4bb3068d819 -r 22b87ab47d3b src/HOL/ex/Nominal2_Dummy.thy --- a/src/HOL/ex/Nominal2_Dummy.thy Thu Oct 30 23:14:11 2014 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,22 +0,0 @@ -header \Dummy theory to anticipate AFP/Nominal2 keywords\ (* Proof General legacy *) - -theory Nominal2_Dummy -imports Main -keywords - "nominal_datatype" :: thy_decl and - "nominal_function" "nominal_inductive" "nominal_termination" :: thy_goal and - "atom_decl" "equivariance" :: thy_decl and - "avoids" "binds" -begin - -ML \ -Outer_Syntax.command @{command_spec "nominal_datatype"} "dummy" Scan.fail; -Outer_Syntax.command @{command_spec "nominal_function"} "dummy" Scan.fail; -Outer_Syntax.command @{command_spec "nominal_inductive"} "dummy" Scan.fail; -Outer_Syntax.command @{command_spec "nominal_termination"} "dummy" Scan.fail; -Outer_Syntax.command @{command_spec "atom_decl"} "dummy" Scan.fail; -Outer_Syntax.command @{command_spec "equivariance"} "dummy" Scan.fail; -\ - -end - diff -r f4bb3068d819 -r 22b87ab47d3b src/Pure/General/secure.ML --- a/src/Pure/General/secure.ML Thu Oct 30 23:14:11 2014 +0100 +++ b/src/Pure/General/secure.ML Fri Oct 31 11:18:17 2014 +0100 @@ -13,7 +13,6 @@ val use_text: use_context -> int * string -> bool -> string -> unit val use_file: use_context -> bool -> string -> unit val toplevel_pp: string list -> string -> unit - val PG_setup: unit -> unit val commit: unit -> unit end; @@ -53,8 +52,5 @@ fun commit () = use_global "commit();"; (*commit is dynamically bound!*) -fun PG_setup () = - use_global "val change = Unsynchronized.change; structure ThyLoad = ProofGeneral.ThyLoad;"; - end; diff -r f4bb3068d819 -r 22b87ab47d3b src/Pure/Pure.thy --- a/src/Pure/Pure.thy Thu Oct 30 23:14:11 2014 +0100 +++ b/src/Pure/Pure.thy Fri Oct 31 11:18:17 2014 +0100 @@ -100,9 +100,6 @@ and "extract_type" "extract" :: thy_decl and "find_theorems" "find_consts" :: diag and "named_theorems" :: thy_decl - and "ProofGeneral.process_pgip" "ProofGeneral.pr" "ProofGeneral.undo" - "ProofGeneral.restart" "ProofGeneral.kill_proof" "ProofGeneral.inform_file_processed" - "ProofGeneral.inform_file_retracted" :: control begin ML_file "ML/ml_antiquotations.ML" @@ -117,7 +114,6 @@ ML_file "Tools/class_deps.ML" ML_file "Tools/find_theorems.ML" ML_file "Tools/find_consts.ML" -ML_file "Tools/proof_general_pure.ML" ML_file "Tools/simplifier_trace.ML" ML_file "Tools/named_theorems.ML" diff -r f4bb3068d819 -r 22b87ab47d3b src/Pure/ROOT --- a/src/Pure/ROOT Thu Oct 30 23:14:11 2014 +0100 +++ b/src/Pure/ROOT Fri Oct 31 11:18:17 2014 +0100 @@ -211,7 +211,6 @@ "Tools/build.ML" "Tools/named_thms.ML" "Tools/plugin.ML" - "Tools/proof_general.ML" "assumption.ML" "axclass.ML" "config.ML" diff -r f4bb3068d819 -r 22b87ab47d3b src/Pure/ROOT.ML --- a/src/Pure/ROOT.ML Thu Oct 30 23:14:11 2014 +0100 +++ b/src/Pure/ROOT.ML Fri Oct 31 11:18:17 2014 +0100 @@ -334,7 +334,6 @@ use "Tools/build.ML"; use "Tools/named_thms.ML"; -use "Tools/proof_general.ML"; structure Output: OUTPUT = Output; (*seal system channels!*) diff -r f4bb3068d819 -r 22b87ab47d3b src/Pure/Tools/keywords.scala --- a/src/Pure/Tools/keywords.scala Thu Oct 30 23:14:11 2014 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,179 +0,0 @@ -/* Title: Pure/Tools/keywords.scala - Author: Makarius - -Generate keyword files for Emacs Proof General. -*/ - -/*Proof General legacy*/ - -package isabelle - - -import scala.collection.mutable - - -object Keywords -{ - /* keywords */ - - private val convert = Map( - "thy_begin" -> "theory-begin", - "thy_end" -> "theory-end", - "thy_heading1" -> "theory-heading", - "thy_heading2" -> "theory-heading", - "thy_heading3" -> "theory-heading", - "thy_heading4" -> "theory-heading", - "thy_load" -> "theory-decl", - "thy_decl" -> "theory-decl", - "thy_decl_block" -> "theory-decl", - "thy_goal" -> "theory-goal", - "qed_script" -> "qed", - "qed_block" -> "qed-block", - "qed_global" -> "qed-global", - "prf_heading2" -> "proof-heading", - "prf_heading3" -> "proof-heading", - "prf_heading4" -> "proof-heading", - "prf_goal" -> "proof-goal", - "prf_block" -> "proof-block", - "prf_open" -> "proof-open", - "prf_close" -> "proof-close", - "prf_chain" -> "proof-chain", - "prf_decl" -> "proof-decl", - "prf_asm" -> "proof-asm", - "prf_asm_goal" -> "proof-asm-goal", - "prf_asm_goal_script" -> "proof-asm-goal", - "prf_script" -> "proof-script" - ).withDefault((s: String) => s) - - private val emacs_kinds = List( - "major", - "minor", - "control", - "diag", - "theory-begin", - "theory-switch", - "theory-end", - "theory-heading", - "theory-decl", - "theory-script", - "theory-goal", - "qed", - "qed-block", - "qed-global", - "proof-heading", - "proof-goal", - "proof-block", - "proof-open", - "proof-close", - "proof-chain", - "proof-decl", - "proof-asm", - "proof-asm-goal", - "proof-script") - - def keywords( - options: Options, - name: String = "", - dirs: List[Path] = Nil, - sessions: List[String] = Nil) - { - val relevant_sessions = - for { - (name, content) <- - Build.session_dependencies(options, false, dirs, sessions).deps.toList - keywords = content.keywords - if !keywords.isEmpty - } yield (name, keywords) - - val keywords_raw = - (Map.empty[String, Set[String]].withDefaultValue(Set.empty) /: relevant_sessions) { - case (map, (_, ks)) => - (map /: ks) { - case (m, (name, Some(((kind, _), _)), _)) => - m + (name -> (m(name) + convert(kind))) - case (m, (name, None, _)) => - m + (name -> (m(name) + "minor")) - } - } - - val keywords_unique = - for ((name, kinds) <- keywords_raw) yield { - kinds.toList match { - case List(kind) => (name, kind) - case _ => - (kinds - "minor").toList match { - case List(kind) => (name, kind) - case _ => - error("Inconsistent declaration of keyword " + quote(name) + ": " + - kinds.toList.sorted.mkString(" vs ")) - } - } - } - - val output = - { - val out = new mutable.StringBuilder - - out ++= ";;\n" - out ++= ";; Keyword classification tables for Isabelle/Isar.\n" - out ++= ";; Generated from " + relevant_sessions.map(_._1).sorted.mkString(" + ") + ".\n" - out ++= ";; *** DO NOT EDIT *** DO NOT EDIT *** DO NOT EDIT ***\n" - out ++= ";;\n" - - for (kind <- emacs_kinds) { - val names = - (for { - (name, k) <- keywords_unique.iterator - if (if (kind == "major") k != "minor" else k == kind) - if kind != "minor" || Symbol.is_ascii_identifier(name) - } yield name).toList.sorted - - out ++= "\n(defconst isar-keywords-" + kind - out ++= "\n '(" - out ++= - names.map(name => quote("""[\.\*\+\?\[\]\^\$]""".r replaceAllIn (name, """\\\\$0"""))) - .mkString("\n ") - out ++= "))\n" - } - - out ++= "\n(provide 'isar-keywords)\n" - - out.toString - } - - val file = if (name == "") "isar-keywords.el" else "isar-keywords-" + name + ".el" - Output.writeln(file) - File.write(Path.explode(file), output) - } - - - /* administrative update_keywords */ - - def update_keywords(options: Options) - { - val tree = Build.find_sessions(options) - - def chapter(ch: String): List[String] = - for ((name, info) <- tree.topological_order if info.chapter == ch) yield name - - keywords(options, sessions = chapter("HOL")) - keywords(options, name = "ZF", sessions = chapter("ZF")) - } - - - /* command line entry point */ - - def main(args: Array[String]) - { - Command_Line.tool0 { - args.toList match { - case "keywords" :: name :: Command_Line.Chunks(dirs, sessions) => - keywords(Options.init(), name, dirs.map(Path.explode), sessions) - case "update_keywords" :: Nil => - update_keywords(Options.init()) - case _ => error("Bad arguments:\n" + cat_lines(args)) - } - } - } -} - diff -r f4bb3068d819 -r 22b87ab47d3b src/Pure/Tools/proof_general.ML --- a/src/Pure/Tools/proof_general.ML Thu Oct 30 23:14:11 2014 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,443 +0,0 @@ -(* Title: Pure/Tools/proof_general.ML - Author: David Aspinall - Author: Makarius - -Isabelle/Isar configuration for Proof General / Emacs. -See also http://proofgeneral.inf.ed.ac.uk -*) - -(*Proof General legacy*) - -signature PROOF_GENERAL = -sig - type category = string - val category_display: category - val category_advanced_display: category - val category_tracing: category - val category_proof: category - type pgiptype = string - val pgipbool: pgiptype - val pgipint: pgiptype - val pgipfloat: pgiptype - val pgipstring: pgiptype - val preference: category -> string option -> - (unit -> string) -> (string -> unit) -> string -> string -> string -> unit - val preference_bool: category -> string option -> - bool Unsynchronized.ref -> string -> string -> unit - val preference_int: category -> string option -> - int Unsynchronized.ref -> string -> string -> unit - val preference_real: category -> string option -> - real Unsynchronized.ref -> string -> string -> unit - val preference_string: category -> string option -> - string Unsynchronized.ref -> string -> string -> unit - val preference_option: category -> string option -> string -> string -> string -> unit - val process_pgip: string -> unit - val tell_clear_goals: unit -> unit - val tell_clear_response: unit -> unit - val inform_file_processed: string -> unit - val inform_file_retracted: string -> unit - val master_path: Path.T Unsynchronized.ref - structure ThyLoad: sig val add_path: string -> unit end - val thm_deps: bool Unsynchronized.ref - val proof_generalN: string - val init: unit -> unit - val restart: unit -> unit -end; - -structure ProofGeneral: PROOF_GENERAL = -struct - -(** preferences **) - -(* type preference *) - -type category = string; -val category_display = "Display"; -val category_advanced_display = "Advanced Display"; -val category_tracing = "Tracing"; -val category_proof = "Proof"; - -type pgiptype = string; -val pgipbool = "pgipbool"; -val pgipint = "pgipint"; -val pgipfloat = "pgipint"; (*NB: PG 3.7.x and 4.0 lack pgipfloat, but accept floats as pgipint*) -val pgipstring = "pgipstring"; - -type preference = - {category: string, - override: string option, - descr: string, - pgiptype: pgiptype, - get: unit -> string, - set: string -> unit}; - - -(* global preferences *) - -local - val preferences = - Synchronized.var "ProofGeneral.preferences" ([]: (string * preference) list); -in - -fun add_preference name pref = - Synchronized.change preferences (fn prefs => - (if not (AList.defined (op =) prefs name) then () - else warning ("Redefining ProofGeneral preference: " ^ quote name); - AList.update (op =) (name, pref) prefs)); - -fun set_preference name value = - (case AList.lookup (op =) (Synchronized.value preferences) name of - SOME {set, ...} => set value - | NONE => error ("Unknown ProofGeneral preference: " ^ quote name)); - -fun all_preferences () = - rev (Synchronized.value preferences) - |> map (fn (name, {category, descr, pgiptype, get, ...}) => - (category, {name = name, descr = descr, default = get (), pgiptype = pgiptype})) - |> AList.group (op =); - -fun init_preferences () = - Synchronized.value preferences - |> List.app (fn (_, {set, override = SOME value, ...}) => set value | _ => ()); - -end; - - - -(* raw preferences *) - -fun preference category override get set typ name descr = - add_preference name - {category = category, override = override, descr = descr, pgiptype = typ, get = get, set = set}; - -fun preference_ref category override read write typ r = - preference category override (fn () => read (! r)) (fn x => r := write x) typ; - -fun preference_bool x y = preference_ref x y Markup.print_bool Markup.parse_bool pgipbool; -fun preference_int x y = preference_ref x y Markup.print_int Markup.parse_int pgipint; -fun preference_real x y = preference_ref x y Markup.print_real Markup.parse_real pgipfloat; -fun preference_string x y = preference_ref x y I I pgipstring; - - -(* system options *) - -fun preference_option category override option_name pgip_name descr = - let - val typ = Options.default_typ option_name; - val pgiptype = - if typ = Options.boolT then pgipbool - else if typ = Options.intT then pgipint - else if typ = Options.realT then pgipfloat - else pgipstring; - in - add_preference pgip_name - {category = category, - override = override, - descr = descr, - pgiptype = pgiptype, - get = fn () => Options.get_default option_name, - set = Options.put_default option_name} - end; - - -(* minimal PGIP support for , , *) - -local - -fun get_attr attrs name = - (case Properties.get attrs name of - SOME value => value - | NONE => raise Fail ("Missing attribute: " ^ quote name)); - -fun attr x y = [(x, y)] : XML.attributes; - -fun opt_attr _ NONE = [] - | opt_attr name (SOME value) = attr name value; - -val pgip_id = "dummy"; -val pgip_serial = Counter.make (); - -fun output_pgip refid refseq content = - XML.Elem (("pgip", - attr "tag" "Isabelle/Isar" @ - attr "id" pgip_id @ - opt_attr "destid" refid @ - attr "class" "pg" @ - opt_attr "refid" refid @ - attr "refseq" refseq @ - attr "seq" (string_of_int (pgip_serial ()))), content) - |> XML.string_of - |> Output.urgent_message; - - -fun invalid_pgip () = raise Fail "Invalid PGIP packet"; - -fun haspref {name, descr, default, pgiptype} = - XML.Elem (("haspref", [("name", name), ("descr", descr), ("default", default)]), - [XML.Elem ((pgiptype, []), [])]); - -fun process_element refid refseq (XML.Elem (("askprefs", _), _)) = - all_preferences () |> List.app (fn (category, prefs) => - output_pgip refid refseq - [XML.Elem (("hasprefs", [("prefcategory", category)]), map haspref prefs)]) - | process_element _ _ (XML.Elem (("setpref", attrs), data)) = - let - val name = - (case Properties.get attrs "name" of - SOME name => name - | NONE => invalid_pgip ()); - val value = XML.content_of data; - in set_preference name value end - | process_element _ _ _ = invalid_pgip (); - -in - -fun process_pgip str = - (case XML.parse str of - XML.Elem (("pgip", attrs), pgips) => - let - val class = get_attr attrs "class"; - val dest = Properties.get attrs "destid"; - val refid = Properties.get attrs "id"; - val refseq = get_attr attrs "seq"; - val processit = - (case dest of - NONE => class = "pa" - | SOME id => id = pgip_id); - in if processit then List.app (process_element refid refseq) pgips else () end - | _ => invalid_pgip ()) - handle Fail msg => raise Fail (msg ^ "\n" ^ str); - -end; - - -(** messages **) - -(* render markup *) - -fun special ch = chr 1 ^ ch; - -local - -fun render_trees ts = fold render_tree ts -and render_tree t = - (case XML.unwrap_elem t of - SOME (_, ts) => render_trees ts - | NONE => - (case t of - XML.Text s => Buffer.add s - | XML.Elem ((name, props), ts) => - let - val (bg, en) = - if null ts then Markup.no_output - else if name = Markup.stateN then (special "O" ^ "\n", "\n" ^ special "P") - else if name = Markup.sendbackN then (special "W", special "X") - else if name = Markup.intensifyN then (special "0", special "1") - else if name = Markup.informationN then ("\n" ^ special "0", special "1") - else if name = Markup.tfreeN then (special "C", special "A") - else if name = Markup.tvarN then (special "D", special "A") - else if name = Markup.freeN then (special "E", special "A") - else if name = Markup.boundN then (special "F", special "A") - else if name = Markup.varN then (special "G", special "A") - else if name = Markup.skolemN then (special "H", special "A") - else - (case Markup.get_entity_kind (name, props) of - SOME kind => - if kind = Markup.classN then (special "B", special "A") - else Markup.no_output - | NONE => Markup.no_output); - in Buffer.add bg #> render_trees ts #> Buffer.add en end)); - -in - -fun render text = - Buffer.content (render_trees (YXML.parse_body text) Buffer.empty); - -end; - - -(* hooks *) - -fun message bg en prfx body = - (case render (implode body) of - "" => () - | s => Output.physical_writeln (enclose bg en (prefix_lines prfx s))); - -fun setup_messages () = - (Output.writeln_fn := message "" "" ""; - Output.status_fn := (fn _ => ()); - Output.report_fn := (fn _ => ()); - Output.urgent_message_fn := message (special "I") (special "J") ""; - Output.tracing_fn := message (special "I" ^ special "V") (special "J") ""; - Output.warning_fn := message (special "K") (special "L") "### "; - Output.error_message_fn := (fn (_, s) => message (special "M") (special "N") "*** " s); - Output.prompt_fn := (fn s => Output.physical_stdout (render s ^ special "S"))); - - -(* notification *) - -fun emacs_notify s = message (special "I") (special "J") "" [s]; - -fun tell_clear_goals () = - emacs_notify "Proof General, please clear the goals buffer."; - -fun tell_clear_response () = - emacs_notify "Proof General, please clear the response buffer."; - -fun tell_file_loaded path = - emacs_notify ("Proof General, this file is loaded: " ^ quote (File.platform_path path)); - -fun tell_file_retracted path = - emacs_notify ("Proof General, you can unlock the file " ^ quote (File.platform_path path)); - - - -(** theory loader **) - -(* global master path *) - -val master_path = Unsynchronized.ref Path.current; - -(*fake old ThyLoad -- with new semantics*) -structure ThyLoad = -struct - fun add_path path = master_path := Path.explode path; -end; - - -(* actions *) - -local - -fun trace_action action name = - if action = Thy_Info.Update then - List.app tell_file_loaded (Thy_Info.loaded_files name) - else if action = Thy_Info.Remove then - List.app tell_file_retracted (Thy_Info.loaded_files name) - else (); - -in - fun setup_thy_loader () = Thy_Info.add_hook trace_action; - fun sync_thy_loader () = List.app (trace_action Thy_Info.Update) (Thy_Info.get_names ()); -end; - - -(* get informed about files *) - -(*liberal low-level version*) -val thy_name = perhaps (try (unsuffix ".thy")) o List.last o space_explode "/"; - -val inform_file_retracted = Thy_Info.kill_thy o thy_name; - -fun inform_file_processed file = - let - val name = thy_name file; - val _ = name = "" andalso error ("Bad file name: " ^ quote file); - val _ = - Thy_Info.register_thy (Toplevel.end_theory Position.none (Isar.state ())) - handle ERROR msg => - (warning (cat_lines ["Failed to register theory: " ^ quote name, msg]); - tell_file_retracted (Resources.thy_path (Path.basic name))) - val _ = Isar.init (); - in () end; - - - -(** theorem dependencies **) - -(* thm_deps *) - -local - -fun add_proof_body (PBody {thms, ...}) = - thms |> fold (fn (_, (name, _, _)) => name <> "" ? Symtab.update (name, ())); - -fun add_thm th = - (case Thm.proof_body_of th of - PBody {proof = PThm (_, ((name, _, _), body)), ...} => - if Thm.has_name_hint th andalso Thm.get_name_hint th = name - then add_proof_body (Future.join body) - else I - | body => add_proof_body body); - -in - -fun get_thm_deps ths = - let - (* FIXME proper derivation names!? *) - val names = map Thm.get_name_hint (filter Thm.has_name_hint ths); - val deps = Symtab.keys (fold add_thm ths Symtab.empty); - in (names, deps) end; - -end; - - -(* report via hook *) - -val thm_deps = Unsynchronized.ref false; - -local - -val spaces_quote = space_implode " " o map quote; - -fun thm_deps_message (thms, deps) = - emacs_notify ("Proof General, theorem dependencies of " ^ thms ^ " are " ^ deps); - -in - -fun setup_present_hook () = Toplevel.add_hook (fn _ => fn state => fn state' => - if ! thm_deps andalso can Toplevel.theory_of state andalso Toplevel.is_theory state' - then - let - val prev_facts = Global_Theory.facts_of (Toplevel.theory_of state); - val facts = Global_Theory.facts_of (Toplevel.theory_of state'); - val (names, deps) = get_thm_deps (maps #2 (Facts.dest_static true [prev_facts] facts)); - in - if null names orelse null deps then () - else thm_deps_message (spaces_quote names, spaces_quote deps) - end - else ()); - -end; - - - -(** startup **) - -(* init *) - -val proof_generalN = "ProofGeneral"; - -val initialized = Unsynchronized.ref false; - -fun init () = - (if ! initialized then () - else - (Output.add_mode Symbol.xsymbolsN Symbol.output Output.default_escape; - Output.add_mode proof_generalN Output.default_output Output.default_escape; - Markup.add_mode proof_generalN YXML.output_markup; - setup_messages (); - setup_thy_loader (); - setup_present_hook (); - initialized := true); - init_preferences (); - sync_thy_loader (); - Unsynchronized.change print_mode (update (op =) proof_generalN); - Secure.PG_setup (); - Isar.toplevel_loop TextIO.stdIn - {init = true, welcome = true, sync = true, secure = Secure.is_secure ()}); - - -(* restart *) - -val welcome = Output.urgent_message o Session.welcome; - -fun restart () = - (sync_thy_loader (); - tell_clear_goals (); - tell_clear_response (); - Isar.init (); - welcome ()); - -end; - diff -r f4bb3068d819 -r 22b87ab47d3b src/Pure/build-jars --- a/src/Pure/build-jars Thu Oct 30 23:14:11 2014 +0100 +++ b/src/Pure/build-jars Fri Oct 31 11:18:17 2014 +0100 @@ -90,7 +90,6 @@ Tools/build_doc.scala Tools/check_source.scala Tools/doc.scala - Tools/keywords.scala Tools/main.scala Tools/ml_statistics.scala Tools/print_operation.scala diff -r f4bb3068d819 -r 22b87ab47d3b src/Pure/pure_syn.ML --- a/src/Pure/pure_syn.ML Thu Oct 30 23:14:11 2014 +0100 +++ b/src/Pure/pure_syn.ML Fri Oct 31 11:18:17 2014 +0100 @@ -11,8 +11,7 @@ Outer_Syntax.command (("theory", Keyword.tag_theory Keyword.thy_begin), @{here}) "begin theory" (Thy_Header.args >> (fn header => - Toplevel.init_theory - (fn () => Thy_Info.toplevel_begin_theory (! ProofGeneral.master_path) header))); + Toplevel.init_theory (fn () => Thy_Info.toplevel_begin_theory Path.current header))); val _ = Outer_Syntax.command diff -r f4bb3068d819 -r 22b87ab47d3b src/Tools/quickcheck.ML --- a/src/Tools/quickcheck.ML Thu Oct 30 23:14:11 2014 +0100 +++ b/src/Tools/quickcheck.ML Fri Oct 31 11:18:17 2014 +0100 @@ -90,16 +90,6 @@ val unknownN = "unknown"; -(* preferences *) - -val _ = - ProofGeneral.preference_option ProofGeneral.category_tracing - NONE - @{system_option auto_quickcheck} - "auto-quickcheck" - "Run Quickcheck automatically"; - - (* quickcheck report *) datatype report = Report of diff -r f4bb3068d819 -r 22b87ab47d3b src/Tools/solve_direct.ML --- a/src/Tools/solve_direct.ML Thu Oct 30 23:14:11 2014 +0100 +++ b/src/Tools/solve_direct.ML Fri Oct 31 11:18:17 2014 +0100 @@ -34,13 +34,6 @@ val max_solutions = Unsynchronized.ref 5; -val _ = - ProofGeneral.preference_option ProofGeneral.category_tracing - NONE - @{system_option auto_solve_direct} - "auto-solve-direct" - ("Run " ^ quote solve_directN ^ " automatically"); - (* solve_direct command *) diff -r f4bb3068d819 -r 22b87ab47d3b src/Tools/try.ML --- a/src/Tools/try.ML Thu Oct 30 23:14:11 2014 +0100 +++ b/src/Tools/try.ML Fri Oct 31 11:18:17 2014 +0100 @@ -27,16 +27,6 @@ val tryN = "try" -(* preferences *) - -val _ = - ProofGeneral.preference_option ProofGeneral.category_tracing - (SOME "4.0") - @{system_option auto_time_limit} - "auto-try-time-limit" - "Time limit for automatically tried tools (in seconds)" - - (* helpers *) fun serial_commas _ [] = ["??"]