# HG changeset patch # User wenzelm # Date 1414795914 -3600 # Node ID cc1e03929685b16c46378ff6e0c0afb75cc7452b # Parent e16712bb1d413660ed44e8d5cb03cfcedccefa6d# Parent b0ccc7e1e7f39a995a99acc7e0b73a4c632244a2 merged diff -r e16712bb1d41 -r cc1e03929685 Admin/ProofGeneral/3.7.1.1/interface --- a/Admin/ProofGeneral/3.7.1.1/interface Fri Oct 31 17:01:54 2014 +0000 +++ /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 e16712bb1d41 -r cc1e03929685 Admin/ProofGeneral/3.7.1.1/isar-antiq-regexp.patch --- a/Admin/ProofGeneral/3.7.1.1/isar-antiq-regexp.patch Fri Oct 31 17:01:54 2014 +0000 +++ /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 e16712bb1d41 -r cc1e03929685 Admin/ProofGeneral/3.7.1.1/menu.patch --- a/Admin/ProofGeneral/3.7.1.1/menu.patch Fri Oct 31 17:01:54 2014 +0000 +++ /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 e16712bb1d41 -r cc1e03929685 Admin/ProofGeneral/3.7.1.1/progname.patch --- a/Admin/ProofGeneral/3.7.1.1/progname.patch Fri Oct 31 17:01:54 2014 +0000 +++ /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 e16712bb1d41 -r cc1e03929685 Admin/ProofGeneral/3.7.1.1/timeout.patch --- a/Admin/ProofGeneral/3.7.1.1/timeout.patch Fri Oct 31 17:01:54 2014 +0000 +++ /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 e16712bb1d41 -r cc1e03929685 Admin/ProofGeneral/3.7.1.1/version.patch --- a/Admin/ProofGeneral/3.7.1.1/version.patch Fri Oct 31 17:01:54 2014 +0000 +++ /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 e16712bb1d41 -r cc1e03929685 Admin/components/optional --- a/Admin/components/optional Fri Oct 31 17:01:54 2014 +0000 +++ b/Admin/components/optional Fri Oct 31 23:51:54 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 e16712bb1d41 -r cc1e03929685 Admin/lib/Tools/update_keywords --- a/Admin/lib/Tools/update_keywords Fri Oct 31 17:01:54 2014 +0000 +++ /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 e16712bb1d41 -r cc1e03929685 NEWS --- a/NEWS Fri Oct 31 17:01:54 2014 +0000 +++ b/NEWS Fri Oct 31 23:51:54 2014 +0100 @@ -187,6 +187,9 @@ *** System *** +* Support for Proof General and Isar TTY loop 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 e16712bb1d41 -r cc1e03929685 bin/isabelle_process --- a/bin/isabelle_process Fri Oct 31 17:01:54 2014 +0000 +++ b/bin/isabelle_process Fri Oct 31 23:51:54 2014 +0100 @@ -26,9 +26,7 @@ echo "Usage: $PRG [OPTIONS] [INPUT] [OUTPUT]" echo 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" @@ -58,9 +56,7 @@ # options -ISAR="" OPTIONS_FILE="" -PROOFGENERAL="" SECURE="" WRAPPER_SOCKET="" WRAPPER_FIFOS="" @@ -71,18 +67,12 @@ READONLY="" NOWRITE="" -while getopts "IO:PST:W:e:m:o:qrw" OPT +while getopts "O:ST:W:e:m:o:qrw" OPT do case "$OPT" in - I) - ISAR=true - ;; O) OPTIONS_FILE="$OPTARG" ;; - P) - PROOFGENERAL=true - ;; S) SECURE=true ;; @@ -213,8 +203,6 @@ [ -n "$SECURE" ] && MLTEXT="$MLTEXT; Secure.set_secure ();" -NICE="nice" - if [ -n "$WRAPPER_SOCKET" ]; then MLTEXT="$MLTEXT; Isabelle_Process.init_socket \"$WRAPPER_SOCKET\";" elif [ -n "$WRAPPER_FIFOS" ]; then @@ -237,21 +225,14 @@ 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 - MLTEXT="$MLTEXT; Isar.main ();" - else - NICE="" - fi fi export INFILE OUTFILE MLTEXT TERMINATE NOWRITE ISABELLE_PID ISABELLE_TMP ISABELLE_PROCESS_OPTIONS if [ -f "$ISABELLE_HOME/lib/scripts/run-$ML_SYSTEM" ]; then - $NICE "$ISABELLE_HOME/lib/scripts/run-$ML_SYSTEM" + "$ISABELLE_HOME/lib/scripts/run-$ML_SYSTEM" else - $NICE "$ISABELLE_HOME/lib/scripts/run-$ML_SYSTEM_BASE" + "$ISABELLE_HOME/lib/scripts/run-$ML_SYSTEM_BASE" fi RC="$?" diff -r e16712bb1d41 -r cc1e03929685 etc/isar-keywords-ZF.el --- a/etc/isar-keywords-ZF.el Fri Oct 31 17:01:54 2014 +0000 +++ /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 e16712bb1d41 -r cc1e03929685 etc/isar-keywords.el --- a/etc/isar-keywords.el Fri Oct 31 17:01:54 2014 +0000 +++ /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 e16712bb1d41 -r cc1e03929685 etc/options --- a/etc/options Fri Oct 31 17:01:54 2014 +0000 +++ b/etc/options Fri Oct 31 23:51:54 2014 +0100 @@ -90,9 +90,6 @@ option condition : string = "" -- "required environment variables for subsequent theories (separated by commas)" -option timing : bool = false - -- "global timing of toplevel command execution and theory processing" - option timeout : real = 0 -- "timeout for session build job (seconds > 0)" diff -r e16712bb1d41 -r cc1e03929685 lib/Tools/keywords --- a/lib/Tools/keywords Fri Oct 31 17:01:54 2014 +0000 +++ /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 e16712bb1d41 -r cc1e03929685 src/Doc/Classes/Classes.thy --- a/src/Doc/Classes/Classes.thy Fri Oct 31 17:01:54 2014 +0000 +++ b/src/Doc/Classes/Classes.thy Fri Oct 31 23:51:54 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 e16712bb1d41 -r cc1e03929685 src/Doc/Implementation/ML.thy --- a/src/Doc/Implementation/ML.thy Fri Oct 31 17:01:54 2014 +0000 +++ b/src/Doc/Implementation/ML.thy Fri Oct 31 23:51:54 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 e16712bb1d41 -r cc1e03929685 src/Doc/Isar_Ref/Inner_Syntax.thy --- a/src/Doc/Isar_Ref/Inner_Syntax.thy Fri Oct 31 17:01:54 2014 +0000 +++ b/src/Doc/Isar_Ref/Inner_Syntax.thy Fri Oct 31 23:51:54 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 e16712bb1d41 -r cc1e03929685 src/Doc/Isar_Ref/Outer_Syntax.thy --- a/src/Doc/Isar_Ref/Outer_Syntax.thy Fri Oct 31 17:01:54 2014 +0000 +++ b/src/Doc/Isar_Ref/Outer_Syntax.thy Fri Oct 31 23:51:54 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 e16712bb1d41 -r cc1e03929685 src/Doc/System/Basics.thy --- a/src/Doc/System/Basics.thy Fri Oct 31 17:01:54 2014 +0000 +++ b/src/Doc/System/Basics.thy Fri Oct 31 23:51:54 2014 +0100 @@ -361,9 +361,7 @@ Usage: isabelle_process [OPTIONS] [INPUT] [OUTPUT] 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 @@ -435,11 +433,6 @@ system options as a file in YXML format (according to the Isabelle/Scala function @{verbatim isabelle.Options.encode}). - \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 Isabelle/Scala, see also @{file diff -r e16712bb1d41 -r cc1e03929685 src/Doc/Tutorial/Documents/Documents.thy --- a/src/Doc/Tutorial/Documents/Documents.thy Fri Oct 31 17:01:54 2014 +0000 +++ b/src/Doc/Tutorial/Documents/Documents.thy Fri Oct 31 23:51:54 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 e16712bb1d41 -r cc1e03929685 src/Doc/Tutorial/ToyList/ToyList_Test.thy --- a/src/Doc/Tutorial/ToyList/ToyList_Test.thy Fri Oct 31 17:01:54 2014 +0000 +++ b/src/Doc/Tutorial/ToyList/ToyList_Test.thy Fri Oct 31 23:51:54 2014 +0100 @@ -3,10 +3,11 @@ begin ML {* - map (File.read o Path.append (Resources.master_directory @{theory}) o Path.explode) - ["ToyList1.txt", "ToyList2.txt"] - |> implode - |> Thy_Info.script_thy Position.start + let val text = + map (File.read o Path.append (Resources.master_directory @{theory}) o Path.explode) + ["ToyList1.txt", "ToyList2.txt"] + |> implode + in Thy_Info.script_thy Position.start text @{theory BNF_Least_Fixpoint} end *} end diff -r e16712bb1d41 -r cc1e03929685 src/Doc/Tutorial/Types/Overloading.thy --- a/src/Doc/Tutorial/Types/Overloading.thy Fri Oct 31 17:01:54 2014 +0000 +++ b/src/Doc/Tutorial/Types/Overloading.thy Fri Oct 31 23:51:54 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 e16712bb1d41 -r cc1e03929685 src/HOL/Divides.thy --- a/src/HOL/Divides.thy Fri Oct 31 17:01:54 2014 +0000 +++ b/src/HOL/Divides.thy Fri Oct 31 23:51:54 2014 +0100 @@ -2047,8 +2047,8 @@ val less = @{term "op < :: int \ int \ bool"} val le = @{term "op \ :: int \ int \ bool"} val simps = @{thms arith_simps} @ @{thms rel_simps} @ [@{thm numeral_1_eq_1 [symmetric]}] - fun prove ctxt goal = (writeln "prove"; Goal.prove ctxt [] [] (HOLogic.mk_Trueprop goal) - (K (ALLGOALS (full_simp_tac (put_simpset HOL_basic_ss ctxt addsimps simps))))); + fun prove ctxt goal = Goal.prove ctxt [] [] (HOLogic.mk_Trueprop goal) + (K (ALLGOALS (full_simp_tac (put_simpset HOL_basic_ss ctxt addsimps simps)))); fun binary_proc proc ctxt ct = (case Thm.term_of ct of _ $ t $ u => diff -r e16712bb1d41 -r cc1e03929685 src/HOL/Library/refute.ML --- a/src/HOL/Library/refute.ML Fri Oct 31 17:01:54 2014 +0000 +++ b/src/HOL/Library/refute.ML Fri Oct 31 23:51:54 2014 +0100 @@ -1068,31 +1068,31 @@ ". Available solvers: " ^ commas (map (quote o fst) (SAT_Solver.get_solvers ())) ^ ".") in - Output.urgent_message "Invoking SAT solver..."; + writeln "Invoking SAT solver..."; (case solver fm of SAT_Solver.SATISFIABLE assignment => - (Output.urgent_message ("Model found:\n" ^ print_model ctxt model + (writeln ("Model found:\n" ^ print_model ctxt model (fn i => case assignment i of SOME b => b | NONE => true)); if maybe_spurious then "potential" else "genuine") | SAT_Solver.UNSATISFIABLE _ => - (Output.urgent_message "No model exists."; + (writeln "No model exists."; case next_universe universe sizes minsize maxsize of SOME universe' => find_model_loop universe' - | NONE => (Output.urgent_message + | NONE => (writeln "Search terminated, no larger universe within the given limits."; "none")) | SAT_Solver.UNKNOWN => - (Output.urgent_message "No model found."; + (writeln "No model found."; case next_universe universe sizes minsize maxsize of SOME universe' => find_model_loop universe' - | NONE => (Output.urgent_message + | NONE => (writeln "Search terminated, no larger universe within the given limits."; "unknown"))) handle SAT_Solver.NOT_CONFIGURED => (error ("SAT solver " ^ quote satsolver ^ " is not configured."); "unknown") end handle MAXVARS_EXCEEDED => - (Output.urgent_message ("Search terminated, number of Boolean variables (" + (writeln ("Search terminated, number of Boolean variables (" ^ string_of_int maxvars ^ " allowed) exceeded."); "unknown") @@ -1114,14 +1114,14 @@ maxtime>=0 orelse error ("\"maxtime\" is " ^ string_of_int maxtime ^ ", must be at least 0"); (* enter loop with or without time limit *) - Output.urgent_message ("Trying to find a model that " + writeln ("Trying to find a model that " ^ (if negate then "refutes" else "satisfies") ^ ": " ^ Syntax.string_of_term ctxt t); if maxtime > 0 then ( TimeLimit.timeLimit (Time.fromSeconds maxtime) wrapper () handle TimeLimit.TimeOut => - (Output.urgent_message ("Search terminated, time limit (" ^ + (writeln ("Search terminated, time limit (" ^ string_of_int maxtime ^ (if maxtime=1 then " second" else " seconds") ^ ") exceeded."); check_expect "unknown") @@ -1207,7 +1207,7 @@ val t = th |> prop_of in if Logic.count_prems t = 0 then - (Output.urgent_message "No subgoal!"; "none") + (writeln "No subgoal!"; "none") else let val assms = map term_of (Assumption.all_assms_of ctxt) diff -r e16712bb1d41 -r cc1e03929685 src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML --- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Fri Oct 31 17:01:54 2014 +0000 +++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Fri Oct 31 23:51:54 2014 +0100 @@ -428,7 +428,7 @@ |> tap (fn factss => "Line " ^ str0 (Position.line_of pos) ^ ": " ^ Sledgehammer.string_of_factss factss - |> Output.urgent_message) + |> writeln) val prover = get_prover ctxt prover_name params goal facts val problem = {comment = "", state = st', goal = goal, subgoal = i, diff -r e16712bb1d41 -r cc1e03929685 src/HOL/Mutabelle/mutabelle_extra.ML --- a/src/HOL/Mutabelle/mutabelle_extra.ML Fri Oct 31 17:01:54 2014 +0000 +++ b/src/HOL/Mutabelle/mutabelle_extra.ML Fri Oct 31 23:51:54 2014 +0100 @@ -171,7 +171,7 @@ let val params = [] val res = Refute.refute_term (Proof_Context.init_global thy) params [] t - val _ = Output.urgent_message ("Refute: " ^ res) + val _ = writeln ("Refute: " ^ res) in (rpair []) (case res of "genuine" => GenuineCex @@ -194,7 +194,7 @@ val state = Proof.init ctxt val (res, _) = Nitpick.pick_nits_in_term state (Nitpick_Commands.default_params thy []) Nitpick.Normal 1 1 1 [] [] [] t - val _ = Output.urgent_message ("Nitpick: " ^ res) + val _ = writeln ("Nitpick: " ^ res) in (rpair []) (case res of "genuine" => GenuineCex @@ -343,21 +343,21 @@ (* fun unsafe_invoke_mtd thy (mtd_name, invoke_mtd) t = let - val _ = Output.urgent_message ("Invoking " ^ mtd_name) + val _ = writeln ("Invoking " ^ mtd_name) val ((res, (timing, reports)), time) = cpu_time "total time" (fn () => invoke_mtd thy t handle ERROR s => (tracing s; (Error, ([], NONE)))) - val _ = Output.urgent_message (" Done") + val _ = writeln (" Done") in (res, (time :: timing, reports)) end *) fun safe_invoke_mtd thy (mtd_name, invoke_mtd) t = let - val _ = Output.urgent_message ("Invoking " ^ mtd_name) + val _ = writeln ("Invoking " ^ mtd_name) val (res, timing) = elapsed_time "total time" (fn () => case try (invoke_mtd thy) t of SOME (res, _) => res - | NONE => (Output.urgent_message ("**** PROBLEMS WITH " ^ Syntax.string_of_term_global thy t); + | NONE => (writeln ("**** PROBLEMS WITH " ^ Syntax.string_of_term_global thy t); Error)) - val _ = Output.urgent_message (" Done") + val _ = writeln (" Done") in (res, [timing]) end (* creating entries *) @@ -387,7 +387,7 @@ val mutants = if exec then let - val _ = Output.urgent_message ("BEFORE PARTITION OF " ^ + val _ = writeln ("BEFORE PARTITION OF " ^ string_of_int (length mutants) ^ " MUTANTS") val (execs, noexecs) = List.partition (is_executable_term thy) (take_random (20 * max_mutants) mutants) val _ = tracing ("AFTER PARTITION (" ^ string_of_int (length execs) ^ @@ -404,7 +404,7 @@ |> filter (is_some o try (Thm.cterm_of thy)) |> filter (is_some o try (Syntax.check_term (Proof_Context.init_global thy))) |> take_random max_mutants - val _ = map (fn t => Output.urgent_message ("MUTANT: " ^ Syntax.string_of_term_global thy t)) mutants + val _ = map (fn t => writeln ("MUTANT: " ^ Syntax.string_of_term_global thy t)) mutants in create_entry thy thm exec mutants mtds end @@ -458,7 +458,7 @@ (* theory -> mtd list -> thm list -> string -> unit *) fun mutate_theorems_and_write_report thy (num_mutations, max_mutants) mtds thms file_name = let - val _ = Output.urgent_message "Starting Mutabelle..." + val _ = writeln "Starting Mutabelle..." val ctxt = Proof_Context.init_global thy val path = Path.explode file_name (* for normal report: *) diff -r e16712bb1d41 -r cc1e03929685 src/HOL/ROOT --- a/src/HOL/ROOT Fri Oct 31 17:01:54 2014 +0000 +++ b/src/HOL/ROOT Fri Oct 31 23:51:54 2014 +0100 @@ -600,7 +600,6 @@ Simps_Case_Conv_Examples ML SAT_Examples - Nominal2_Dummy SOS SOS_Cert theories [skip_proofs = false] @@ -759,7 +758,7 @@ Misc_Datatype Misc_Primcorec Misc_Primrec - theories [condition = ISABELLE_FULL_TEST, timing] + theories [condition = ISABELLE_FULL_TEST] Brackin IsaFoR Misc_N2M @@ -1099,6 +1098,6 @@ Some benchmark on large record. *} options [document = false] - theories [condition = ISABELLE_FULL_TEST, timing] + theories [condition = ISABELLE_FULL_TEST] Record_Benchmark diff -r e16712bb1d41 -r cc1e03929685 src/HOL/TPTP/atp_problem_import.ML --- a/src/HOL/TPTP/atp_problem_import.ML Fri Oct 31 17:01:54 2014 +0000 +++ b/src/HOL/TPTP/atp_problem_import.ML Fri Oct 31 23:51:54 2014 +0100 @@ -117,7 +117,7 @@ if falsify then "CounterSatisfiable" else "Satisfiable" else "Unknown") - |> Output.urgent_message + |> writeln val (conjs, (defs, nondefs), ctxt) = read_tptp_file thy snd file_name val params = [("maxtime", string_of_int timeout), @@ -135,7 +135,7 @@ fun SOLVE_TIMEOUT seconds name tac st = let - val _ = Output.urgent_message ("running " ^ name ^ " for " ^ string_of_int seconds ^ " s") + val _ = writeln ("running " ^ name ^ " for " ^ string_of_int seconds ^ " s") val result = TimeLimit.timeLimit (Time.fromSeconds seconds) (fn () => SINGLE (SOLVE tac) st) () handle @@ -143,8 +143,8 @@ | ERROR _ => NONE in (case result of - NONE => (Output.urgent_message ("FAILURE: " ^ name); Seq.empty) - | SOME st' => (Output.urgent_message ("SUCCESS: " ^ name); Seq.single st')) + NONE => (writeln ("FAILURE: " ^ name); Seq.empty) + | SOME st' => (writeln ("SUCCESS: " ^ name); Seq.single st')) end fun nitpick_finite_oracle_tac ctxt timeout i th = @@ -264,7 +264,7 @@ Logic.list_implies (rev defs @ rev nondefs, case conjs of conj :: _ => conj | [] => @{prop False}) fun print_szs_of_success conjs success = - Output.urgent_message ("% SZS status " ^ + writeln ("% SZS status " ^ (if success then if null conjs then "Unsatisfiable" else "Theorem" else diff -r e16712bb1d41 -r cc1e03929685 src/HOL/Tools/Nitpick/nitpick.ML --- a/src/HOL/Tools/Nitpick/nitpick.ML Fri Oct 31 17:01:54 2014 +0000 +++ b/src/HOL/Tools/Nitpick/nitpick.ML Fri Oct 31 23:51:54 2014 +0100 @@ -241,11 +241,11 @@ o Pretty.mark Markup.information else print o Pretty.string_of - val pprint_a = pprint Output.urgent_message - fun pprint_nt f = () |> is_mode_nt mode ? pprint Output.urgent_message o f - fun pprint_v f = () |> verbose ? pprint Output.urgent_message o f + val pprint_a = pprint writeln + fun pprint_nt f = () |> is_mode_nt mode ? pprint writeln o f + fun pprint_v f = () |> verbose ? pprint writeln o f fun pprint_d f = () |> debug ? pprint tracing o f - val print = pprint Output.urgent_message o curry Pretty.blk 0 o pstrs + val print = pprint writeln o curry Pretty.blk 0 o pstrs fun print_t f = () |> mode = TPTP ? print o f (* val print_g = pprint tracing o Pretty.str @@ -1015,8 +1015,8 @@ fun pick_nits_in_term state (params as {timeout, expect, ...}) mode i n step subst def_assm_ts nondef_assm_ts orig_t = let - val print_nt = if is_mode_nt mode then Output.urgent_message else K () - val print_t = if mode = TPTP then Output.urgent_message else K () + val print_nt = if is_mode_nt mode then writeln else K () + val print_t = if mode = TPTP then writeln else K () in if getenv "KODKODI" = "" then (* The "expect" argument is deliberately ignored if Kodkodi is missing so @@ -1068,7 +1068,7 @@ val t = state |> Proof.raw_goal |> #goal |> prop_of in case Logic.count_prems t of - 0 => (Output.urgent_message "No subgoal!"; (noneN, state)) + 0 => (writeln "No subgoal!"; (noneN, state)) | n => let val t = Logic.goal_params t i |> fst diff -r e16712bb1d41 -r cc1e03929685 src/HOL/Tools/Nitpick/nitpick_commands.ML --- a/src/HOL/Tools/Nitpick/nitpick_commands.ML Fri Oct 31 17:01:54 2014 +0000 +++ b/src/HOL/Tools/Nitpick/nitpick_commands.ML Fri Oct 31 23:51:54 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 e16712bb1d41 -r cc1e03929685 src/HOL/Tools/Nitpick/nitpick_hol.ML --- a/src/HOL/Tools/Nitpick/nitpick_hol.ML Fri Oct 31 17:01:54 2014 +0000 +++ b/src/HOL/Tools/Nitpick/nitpick_hol.ML Fri Oct 31 23:51:54 2014 +0100 @@ -2140,8 +2140,7 @@ map (wf_constraint_for_triple rel) triples |> foldr1 s_conj |> HOLogic.mk_Trueprop val _ = if debug then - Output.urgent_message ("Wellfoundedness goal: " ^ - Syntax.string_of_term ctxt prop ^ ".") + writeln ("Wellfoundedness goal: " ^ Syntax.string_of_term ctxt prop ^ ".") else () in diff -r e16712bb1d41 -r cc1e03929685 src/HOL/Tools/Nitpick/nitpick_model.ML --- a/src/HOL/Tools/Nitpick/nitpick_model.ML Fri Oct 31 17:01:54 2014 +0000 +++ b/src/HOL/Tools/Nitpick/nitpick_model.ML Fri Oct 31 23:51:54 2014 +0100 @@ -1059,7 +1059,7 @@ if debug then (if negate then "Genuineness" else "Spuriousness") ^ " goal: " ^ Syntax.string_of_term ctxt prop ^ "." - |> Output.urgent_message + |> writeln else () val goal = prop |> cterm_of thy |> Goal.init diff -r e16712bb1d41 -r cc1e03929685 src/HOL/Tools/Predicate_Compile/predicate_compile_quickcheck.ML --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_quickcheck.ML Fri Oct 31 17:01:54 2014 +0000 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_quickcheck.ML Fri Oct 31 23:51:54 2014 +0100 @@ -360,7 +360,7 @@ fun try_upto_depth ctxt f = let val max_depth = Config.get ctxt Quickcheck.depth - fun message s = if Config.get ctxt Quickcheck.quiet then () else Output.urgent_message s + fun message s = if Config.get ctxt Quickcheck.quiet then () else writeln s fun try' i = if i <= max_depth then let diff -r e16712bb1d41 -r cc1e03929685 src/HOL/Tools/Quickcheck/narrowing_generators.ML --- a/src/HOL/Tools/Quickcheck/narrowing_generators.ML Fri Oct 31 17:01:54 2014 +0000 +++ b/src/HOL/Tools/Quickcheck/narrowing_generators.ML Fri Oct 31 23:51:54 2014 +0100 @@ -221,8 +221,8 @@ fun value (contains_existentials, ((genuine_only, (quiet, verbose)), size)) ctxt cookie (code_modules, _) = let val ((is_genuine, counterexample_of), (get, put, put_ml)) = cookie - fun message s = if quiet then () else Output.urgent_message s - fun verbose_message s = if not quiet andalso verbose then Output.urgent_message s else () + fun message s = if quiet then () else writeln s + fun verbose_message s = if not quiet andalso verbose then writeln s else () val current_size = Unsynchronized.ref 0 val current_result = Unsynchronized.ref Quickcheck.empty_result val tmp_prefix = "Quickcheck_Narrowing" @@ -511,7 +511,7 @@ (maps (map snd) correct_inst_goals) [] end else - (if Config.get ctxt Quickcheck.quiet then () else Output.urgent_message + (if Config.get ctxt Quickcheck.quiet then () else writeln ("Environment variable ISABELLE_GHC is not set. To use narrowing-based quickcheck, please set " ^ "this variable to your GHC Haskell compiler in your settings file. " ^ "To deactivate narrowing-based quickcheck, set quickcheck_narrowing_active to false."); diff -r e16712bb1d41 -r cc1e03929685 src/HOL/Tools/Sledgehammer/async_manager.ML --- a/src/HOL/Tools/Sledgehammer/async_manager.ML Fri Oct 31 17:01:54 2014 +0000 +++ b/src/HOL/Tools/Sledgehammer/async_manager.ML Fri Oct 31 23:51:54 2014 +0100 @@ -106,7 +106,7 @@ tool ^ ": " ^ implode_message (workers |> sort_distinct string_ord, work) |> break_into_chunks - |> List.app Output.urgent_message) + |> List.app writeln) fun check_thread_manager () = Synchronized.change global_state (fn state as {manager, timeout_heap, active, canceling, messages, store} => @@ -178,7 +178,7 @@ val state' = make_state manager timeout_heap [] (killing @ canceling) messages store val _ = if null killing then () - else Output.urgent_message ("Interrupted active " ^ das_wort_worker ^ "s.") + else writeln ("Interrupted active " ^ das_wort_worker ^ "s.") in state' end) fun str_of_time time = string_of_int (Time.toSeconds time) ^ " s" @@ -210,7 +210,7 @@ case map_filter canceling_info canceling of [] => [] | ss => "Interrupting " ^ das_wort_worker ^ "s" :: ss - in Output.urgent_message (space_implode "\n\n" (running @ interrupting)) end + in writeln (space_implode "\n\n" (running @ interrupting)) end fun thread_messages tool das_wort_worker opt_limit = let @@ -222,6 +222,6 @@ (if length tool_store <= limit then ":" else " (" ^ string_of_int limit ^ " displayed):") val ss = tool_store |> chop limit |> #1 |> map (op ^ o snd) - in List.app Output.urgent_message (header :: maps break_into_chunks ss) end + in List.app writeln (header :: maps break_into_chunks ss) end end; diff -r e16712bb1d41 -r cc1e03929685 src/HOL/Tools/Sledgehammer/sledgehammer.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer.ML Fri Oct 31 17:01:54 2014 +0000 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer.ML Fri Oct 31 23:51:54 2014 +0100 @@ -137,7 +137,7 @@ |> commas |> enclose ("Fact" ^ plural_s (length facts) ^ " in " ^ quote name ^ " proof (of " ^ string_of_int (length facts) ^ "): ") "." - |> Output.urgent_message + |> writeln fun spying_str_of_res ({outcome = NONE, used_facts, used_from, ...} : prover_result) = let @@ -230,7 +230,7 @@ else outcome |> Async_Manager.break_into_chunks - |> List.app Output.urgent_message + |> List.app writeln in (outcome_code, state) end else (Async_Manager.thread SledgehammerN birth_time death_time @@ -259,12 +259,12 @@ else (case subgoal_count state of 0 => - ((if blocking then error else Output.urgent_message) "No subgoal!"; (false, (noneN, state))) + ((if blocking then error else writeln) "No subgoal!"; (false, (noneN, state))) | n => let val _ = Proof.assert_backward state val print = - if mode = Normal andalso is_none output_result then Output.urgent_message else K () + if mode = Normal andalso is_none output_result then writeln else K () val ctxt = Proof.context_of state val {facts = chained, goal, ...} = Proof.goal state val (_, hyp_ts, concl_t) = strip_subgoal goal i ctxt diff -r e16712bb1d41 -r cc1e03929685 src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML Fri Oct 31 17:01:54 2014 +0000 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML Fri Oct 31 23:51:54 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 e16712bb1d41 -r cc1e03929685 src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Fri Oct 31 17:01:54 2014 +0000 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Fri Oct 31 23:51:54 2014 +0100 @@ -150,7 +150,7 @@ fun isar_proof_text ctxt debug isar_proofs smt_proofs isar_params (one_line_params as ((used_facts, (_, one_line_play)), banner, subgoal, subgoal_count)) = let - val _ = if debug then Output.urgent_message "Constructing Isar proof..." else () + val _ = if debug then writeln "Constructing Isar proof..." else () fun generate_proof_text () = let diff -r e16712bb1d41 -r cc1e03929685 src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML Fri Oct 31 17:01:54 2014 +0000 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML Fri Oct 31 23:51:54 2014 +0100 @@ -1016,7 +1016,7 @@ val num_isar_deps = length isar_deps in if verbose andalso auto_level = 0 then - Output.urgent_message ("MaSh: " ^ quote prover ^ " on " ^ quote name ^ " with " ^ + writeln ("MaSh: " ^ quote prover ^ " on " ^ quote name ^ " with " ^ string_of_int num_isar_deps ^ " + " ^ string_of_int (length facts - num_isar_deps) ^ " facts.") else @@ -1025,7 +1025,7 @@ {outcome = NONE, used_facts, ...} => (if verbose andalso auto_level = 0 then let val num_facts = length used_facts in - Output.urgent_message ("Found proof with " ^ string_of_int num_facts ^ " fact" ^ + writeln ("Found proof with " ^ string_of_int num_facts ^ " fact" ^ plural_s num_facts ^ ".") end else @@ -1212,7 +1212,7 @@ |> pairself (map fact_of_raw_fact) end -fun mash_unlearn () = (clear_state (); Output.urgent_message "Reset MaSh.") +fun mash_unlearn () = (clear_state (); writeln "Reset MaSh.") fun learn_wrt_access_graph ctxt (name, parents, feats, deps) (accum as (access_G, (fact_xtab, feat_xtab))) = @@ -1361,11 +1361,11 @@ end fun commit last learns relearns flops = - (if debug andalso auto_level = 0 then Output.urgent_message "Committing..." else (); + (if debug andalso auto_level = 0 then writeln "Committing..." else (); map_state ctxt (do_commit (rev learns) relearns flops); if not last andalso auto_level = 0 then let val num_proofs = length learns + length relearns in - Output.urgent_message ("Learned " ^ string_of_int num_proofs ^ " " ^ + writeln ("Learned " ^ string_of_int num_proofs ^ " " ^ (if run_prover then "automatic" else "Isar") ^ " proof" ^ plural_s num_proofs ^ " in the last " ^ string_of_time commit_timeout ^ ".") end @@ -1474,18 +1474,18 @@ fun learn auto_level run_prover = mash_learn_facts ctxt params prover auto_level run_prover one_year facts - |> Output.urgent_message + |> writeln in if run_prover then - (Output.urgent_message ("MaShing through " ^ string_of_int num_facts ^ " fact" ^ + (writeln ("MaShing through " ^ string_of_int num_facts ^ " fact" ^ plural_s num_facts ^ " for automatic proofs (" ^ quote prover ^ " timeout: " ^ string_of_time timeout ^ ").\n\nCollecting Isar proofs first..."); learn 1 false; - Output.urgent_message "Now collecting automatic proofs. This may take several hours. You \ + writeln "Now collecting automatic proofs. This may take several hours. You \ \can safely stop the learning process at any point."; learn 0 true) else - (Output.urgent_message ("MaShing through " ^ string_of_int num_facts ^ " fact" ^ + (writeln ("MaShing through " ^ string_of_int num_facts ^ " fact" ^ plural_s num_facts ^ " for Isar proofs..."); learn 0 false) end @@ -1522,7 +1522,7 @@ Time.toSeconds timeout >= min_secs_for_learning then let val timeout = time_mult learn_timeout_slack timeout in (if verbose then - Output.urgent_message ("Started MaShing through " ^ + writeln ("Started MaShing through " ^ (if exact then "" else "at least ") ^ string_of_int min_num_facts_to_learn ^ " fact" ^ plural_s min_num_facts_to_learn ^ " in the background.") else @@ -1545,7 +1545,7 @@ | num_facts_to_learn => if num_facts_to_learn <= max_facts_to_learn_before_query then mash_learn_facts ctxt params prover 2 false timeout facts - |> (fn "" => () | s => Output.urgent_message (MaShN ^ ": " ^ s)) + |> (fn "" => () | s => writeln (MaShN ^ ": " ^ s)) else maybe_launch_thread true num_facts_to_learn) else diff -r e16712bb1d41 -r cc1e03929685 src/HOL/Tools/Sledgehammer/sledgehammer_prover.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover.ML Fri Oct 31 17:01:54 2014 +0000 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover.ML Fri Oct 31 23:51:54 2014 +0100 @@ -198,7 +198,7 @@ sort_strings (supported_atps thy) @ sort_strings (SMT_Config.available_solvers_of ctxt) |> List.partition (String.isPrefix remote_prefix) in - Output.urgent_message ("Supported provers: " ^ commas (local_provers @ remote_provers) ^ ".") + writeln ("Supported provers: " ^ commas (local_provers @ remote_provers) ^ ".") end fun kill_provers () = Async_Manager.kill_threads SledgehammerN "prover" diff -r e16712bb1d41 -r cc1e03929685 src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML Fri Oct 31 17:01:54 2014 +0000 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML Fri Oct 31 23:51:54 2014 +0100 @@ -250,7 +250,7 @@ quote name ^ " slice #" ^ string_of_int (slice + 1) ^ " with " ^ string_of_int num_facts ^ " fact" ^ plural_s num_facts ^ " for " ^ string_of_time slice_timeout ^ "..." - |> Output.urgent_message + |> writeln else () val readable_names = not (Config.get ctxt atp_full_names) @@ -370,7 +370,7 @@ (used_facts, preferred_methss, fn preplay => let - val _ = if verbose then Output.urgent_message "Generating proof text..." else () + val _ = if verbose then writeln "Generating proof text..." else () fun isar_params () = let diff -r e16712bb1d41 -r cc1e03929685 src/HOL/Tools/Sledgehammer/sledgehammer_prover_minimize.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover_minimize.ML Fri Oct 31 17:01:54 2014 +0000 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover_minimize.ML Fri Oct 31 23:51:54 2014 +0100 @@ -76,7 +76,7 @@ (if n > 0 then ": " ^ (names |> map fst |> sort string_ord |> space_implode " ") else "") end -fun print silent f = if silent then () else Output.urgent_message (f ()) +fun print silent f = if silent then () else writeln (f ()) fun test_facts ({debug, verbose, overlord, spy, provers, max_mono_iters, max_new_mono_instances, type_enc, strict, lam_trans, uncurried_aliases, isar_proofs, compress, try0, smt_proofs, diff -r e16712bb1d41 -r cc1e03929685 src/HOL/Tools/Sledgehammer/sledgehammer_prover_smt.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover_smt.ML Fri Oct 31 17:01:54 2014 +0000 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover_smt.ML Fri Oct 31 23:51:54 2014 +0100 @@ -113,7 +113,7 @@ if debug then quote name ^ " slice " ^ string_of_int slice ^ " with " ^ string_of_int num_facts ^ " fact" ^ plural_s num_facts ^ " for " ^ string_of_time slice_timeout - |> Output.urgent_message + |> writeln else () val birth = Timer.checkRealTimer timer @@ -163,7 +163,7 @@ string_of_atp_failure (failure_of_smt_failure (the outcome)) ^ " Retrying with " ^ num_of_facts new_fact_filter new_num_facts ^ "..." - |> Output.urgent_message + |> writeln else () in @@ -204,7 +204,7 @@ (preferred_methss, fn preplay => let - val _ = if verbose then Output.urgent_message "Generating proof text..." else () + val _ = if verbose then writeln "Generating proof text..." else () fun isar_params () = (verbose, (NONE, NONE), preplay_timeout, compress, try0, minimize, atp_proof (), diff -r e16712bb1d41 -r cc1e03929685 src/HOL/Tools/try0.ML --- a/src/HOL/Tools/try0.ML Fri Oct 31 17:01:54 2014 +0000 +++ b/src/HOL/Tools/try0.ML Fri Oct 31 23:51:54 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 = @@ -131,12 +124,12 @@ if mode = Normal then "Trying " ^ space_implode " " (Try.serial_commas "and" (map (quote o fst) named_methods)) ^ "..." - |> Output.urgent_message + |> writeln else (); (case par_map (fn f => f mode timeout_opt quad st) apply_methods of [] => - (if mode = Normal then Output.urgent_message "No proof found." else (); (false, (noneN, st))) + (if mode = Normal then writeln "No proof found." else (); (false, (noneN, st))) | xs as (name, command, _) :: _ => let val xs = xs |> map (fn (name, _, n) => (n, name)) @@ -159,7 +152,7 @@ |> (if mode = Auto_Try then Proof.goal_message (fn () => Pretty.markup Markup.information [Pretty.str message]) else - tap (fn _ => Output.urgent_message message)))) + tap (fn _ => writeln message)))) end) end; diff -r e16712bb1d41 -r cc1e03929685 src/HOL/ex/Nominal2_Dummy.thy --- a/src/HOL/ex/Nominal2_Dummy.thy Fri Oct 31 17:01:54 2014 +0000 +++ /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 e16712bb1d41 -r cc1e03929685 src/Pure/General/antiquote.ML --- a/src/Pure/General/antiquote.ML Fri Oct 31 17:01:54 2014 +0000 +++ b/src/Pure/General/antiquote.ML Fri Oct 31 23:51:54 2014 +0100 @@ -49,12 +49,12 @@ val scan_txt = Scan.repeat1 ($$$ "@" --| Scan.ahead (~$$ "{") || - Scan.many1 (fn (s, _) => s <> "@" andalso Symbol.is_regular s)) >> flat; + Scan.many1 (fn (s, _) => s <> "@" andalso Symbol.not_eof s)) >> flat; val scan_antiq_body = Scan.trace (Symbol_Pos.scan_string_qq err_prefix || Symbol_Pos.scan_string_bq err_prefix) >> #2 || Scan.trace (Symbol_Pos.scan_cartouche err_prefix) >> #2 || - Scan.one (fn (s, _) => s <> "}" andalso Symbol.is_regular s) >> single; + Scan.one (fn (s, _) => s <> "}" andalso Symbol.not_eof s) >> single; in diff -r e16712bb1d41 -r cc1e03929685 src/Pure/General/output.ML --- a/src/Pure/General/output.ML Fri Oct 31 17:01:54 2014 +0000 +++ b/src/Pure/General/output.ML Fri Oct 31 23:51:54 2014 +0100 @@ -26,11 +26,9 @@ val physical_writeln: output -> unit exception Protocol_Message of Properties.T val writelns: string list -> unit - val urgent_message: string -> unit val error_message': serial * string -> unit val error_message: string -> unit val system_message: string -> unit - val prompt: string -> unit val status: string -> unit val report: string list -> unit val result: Properties.T -> string list -> unit @@ -42,12 +40,10 @@ sig include OUTPUT val writeln_fn: (output list -> unit) Unsynchronized.ref - val urgent_message_fn: (output list -> unit) Unsynchronized.ref val tracing_fn: (output list -> unit) Unsynchronized.ref val warning_fn: (output list -> unit) Unsynchronized.ref val error_message_fn: (serial * output list -> unit) Unsynchronized.ref val system_message_fn: (output list -> unit) Unsynchronized.ref - val prompt_fn: (output -> unit) Unsynchronized.ref val status_fn: (output list -> unit) Unsynchronized.ref val report_fn: (output list -> unit) Unsynchronized.ref val result_fn: (Properties.T -> output list -> unit) Unsynchronized.ref @@ -98,13 +94,11 @@ exception Protocol_Message of Properties.T; val writeln_fn = Unsynchronized.ref (physical_writeln o implode); -val urgent_message_fn = Unsynchronized.ref (fn ss => ! writeln_fn ss); (*Proof General legacy*) val tracing_fn = Unsynchronized.ref (fn ss => ! writeln_fn ss); val warning_fn = Unsynchronized.ref (physical_writeln o prefix_lines "### " o implode); val error_message_fn = Unsynchronized.ref (fn (_: serial, ss) => physical_writeln (prefix_lines "*** " (implode ss))); val system_message_fn = Unsynchronized.ref (fn ss => ! writeln_fn ss); -val prompt_fn = Unsynchronized.ref physical_stdout; (*Proof General legacy*) val status_fn = Unsynchronized.ref (fn _: output list => ()); val report_fn = Unsynchronized.ref (fn _: output list => ()); val result_fn = Unsynchronized.ref (fn _: Properties.T => fn _: output list => ()); @@ -113,13 +107,11 @@ fun writelns ss = ! writeln_fn (map output ss); fun writeln s = writelns [s]; -fun urgent_message s = ! urgent_message_fn [output s]; (*Proof General legacy*) fun tracing s = ! tracing_fn [output s]; fun warning s = ! warning_fn [output s]; fun error_message' (i, s) = ! error_message_fn (i, [output s]); fun error_message s = error_message' (serial (), s); fun system_message s = ! system_message_fn [output s]; -fun prompt s = ! prompt_fn (output s); fun status s = ! status_fn [output s]; fun report ss = ! report_fn (map output ss); fun result props ss = ! result_fn props (map output ss); diff -r e16712bb1d41 -r cc1e03929685 src/Pure/General/position.ML --- a/src/Pure/General/position.ML Fri Oct 31 17:01:54 2014 +0000 +++ b/src/Pure/General/position.ML Fri Oct 31 23:51:54 2014 +0100 @@ -90,7 +90,7 @@ fun advance_count "\n" (i: int, j: int, k: int) = (if_valid i (i + 1), if_valid j (j + 1), k) | advance_count s (i, j, k) = - if Symbol.is_regular s then (i, if_valid j (j + 1), k) + if Symbol.not_eof s then (i, if_valid j (j + 1), k) else (i, j, k); fun invalid_count (i, j, _: int) = diff -r e16712bb1d41 -r cc1e03929685 src/Pure/General/scan.ML --- a/src/Pure/General/scan.ML Fri Oct 31 17:01:54 2014 +0000 +++ b/src/Pure/General/scan.ML Fri Oct 31 23:51:54 2014 +0100 @@ -38,7 +38,6 @@ signature SCAN = sig include BASIC_SCAN - val prompt: string -> ('a -> 'b) -> 'a -> 'b val permissive: ('a -> 'b) -> 'a -> 'b val error: ('a -> 'b) -> 'a -> 'b val catch: ('a -> 'b) -> 'a -> 'b (*exception Fail*) @@ -76,8 +75,8 @@ -> 'b * 'a list -> 'c * ('d * 'a list) val finite: 'a stopper -> ('a list -> 'b * 'a list) -> 'a list -> 'b * 'a list val read: 'a stopper -> ('a list -> 'b * 'a list) -> 'a list -> 'b option - val drain: string -> (string -> 'a -> 'b list * 'a) -> 'b stopper -> - ('c * 'b list -> 'd * ('e * 'b list)) -> ('c * 'b list) * 'a -> ('d * ('e * 'b list)) * 'a + val drain: ('a -> 'b list * 'a) -> 'b stopper -> ('c * 'b list -> 'd * ('e * 'b list)) -> + ('c * 'b list) * 'a -> ('d * ('e * 'b list)) * 'a type lexicon val is_literal: lexicon -> string list -> bool val literal: lexicon -> (string * 'a) list -> (string * 'a) list * (string * 'a) list @@ -98,14 +97,13 @@ type message = unit -> string; -exception MORE of string option; (*need more input (prompt)*) -exception FAIL of message option; (*try alternatives (reason of failure)*) -exception ABORT of message; (*dead end*) +exception MORE of unit; (*need more input*) +exception FAIL of message option; (*try alternatives (reason of failure)*) +exception ABORT of message; (*dead end*) fun !! err scan xs = scan xs handle FAIL msg => raise ABORT (err (xs, msg)); -fun permissive scan xs = scan xs handle MORE _ => raise FAIL NONE | ABORT _ => raise FAIL NONE; -fun strict scan xs = scan xs handle MORE _ => raise FAIL NONE; -fun prompt str scan xs = scan xs handle MORE NONE => raise MORE (SOME str); +fun permissive scan xs = scan xs handle MORE () => raise FAIL NONE | ABORT _ => raise FAIL NONE; +fun strict scan xs = scan xs handle MORE () => raise FAIL NONE; fun error scan xs = scan xs handle ABORT msg => Library.error (msg ()); fun catch scan xs = scan xs @@ -140,11 +138,11 @@ fun fail_with msg_of xs = raise FAIL (SOME (msg_of xs)); fun succeed y xs = (y, xs); -fun some _ [] = raise MORE NONE +fun some _ [] = raise MORE () | some f (x :: xs) = (case f x of SOME y => (y, xs) | _ => raise FAIL NONE); -fun one _ [] = raise MORE NONE +fun one _ [] = raise MORE () | one pred (x :: xs) = if pred x then (x, xs) else raise FAIL NONE; @@ -154,14 +152,14 @@ fun this ys xs = let fun drop_prefix [] xs = xs - | drop_prefix (_ :: _) [] = raise MORE NONE + | drop_prefix (_ :: _) [] = raise MORE () | drop_prefix (y :: ys) (x :: xs) = if (y: string) = x then drop_prefix ys xs else raise FAIL NONE; in (ys, drop_prefix ys xs) end; fun this_string s = this (raw_explode s) >> K s; (*primitive string -- no symbols here!*) -fun many _ [] = raise MORE NONE +fun many _ [] = raise MORE () | many pred (lst as x :: xs) = if pred x then apfst (cons x) (many pred xs) else ([], lst); @@ -265,11 +263,11 @@ (* infinite scans -- draining state-based source *) -fun drain def_prompt get stopper scan ((state, xs), src) = - (scan (state, xs), src) handle MORE prompt => - (case get (the_default def_prompt prompt) src of +fun drain get stopper scan ((state, xs), src) = + (scan (state, xs), src) handle MORE () => + (case get src of ([], _) => (finite' stopper scan (state, xs), src) - | (xs', src') => drain def_prompt get stopper scan ((state, xs @ xs'), src')); + | (xs', src') => drain get stopper scan ((state, xs @ xs'), src')); @@ -292,7 +290,8 @@ let fun finish (SOME (res, rest)) = (rev res, rest) | finish NONE = raise FAIL NONE; - fun scan _ res (Lexicon tab) [] = if Symtab.is_empty tab then finish res else raise MORE NONE + fun scan _ res (Lexicon tab) [] = + if Symtab.is_empty tab then finish res else raise MORE () | scan path res (Lexicon tab) (c :: cs) = (case Symtab.lookup tab (fst c) of SOME (tip, lex) => diff -r e16712bb1d41 -r cc1e03929685 src/Pure/General/secure.ML --- a/src/Pure/General/secure.ML Fri Oct 31 17:01:54 2014 +0000 +++ b/src/Pure/General/secure.ML Fri Oct 31 23:51:54 2014 +0100 @@ -13,8 +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; structure Secure: SECURE = @@ -33,8 +31,6 @@ (** critical operations **) -(* ML evaluation *) - fun secure_mltext () = deny_secure "Cannot evaluate ML source in secure mode"; val raw_use_text = use_text; @@ -46,15 +42,5 @@ fun toplevel_pp path pp = (secure_mltext (); raw_toplevel_pp ML_Parse.global_context path pp); - -(* global evaluation *) - -val use_global = raw_use_text ML_Parse.global_context (0, "") false; - -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 e16712bb1d41 -r cc1e03929685 src/Pure/General/source.ML --- a/src/Pure/General/source.ML Fri Oct 31 17:01:54 2014 +0000 +++ b/src/Pure/General/source.ML Fri Oct 31 23:51:54 2014 +0100 @@ -7,8 +7,6 @@ signature SOURCE = sig type ('a, 'b) source - val default_prompt: string - val set_prompt: string -> ('a, 'b) source -> ('a, 'b) source val get: ('a, 'b) source -> 'a list * ('a, 'b) source val unget: 'a list * ('a, 'b) source -> ('a, 'b) source val get_single: ('a, 'b) source -> ('a * ('a, 'b) source) option @@ -19,7 +17,6 @@ val exhausted: ('a, 'b) source -> ('a, 'a list) source val of_string: string -> (string, string list) source val of_string_limited: int -> string -> (string, substring) source - val tty: TextIO.instream -> (string, unit) source val source': 'a -> 'b Scan.stopper -> ('a * 'b list -> 'c list * ('a * 'b list)) -> (bool * (string -> 'a * 'b list -> 'c list * ('a * 'b list))) option -> ('b, 'e) source -> ('c, 'a * ('b, 'e) source) source @@ -38,37 +35,24 @@ Source of {buffer: 'a list, info: 'b, - prompt: string, - drain: string -> 'b -> 'a list * 'b}; - -fun make_source buffer info prompt drain = - Source {buffer = buffer, info = info, prompt = prompt, drain = drain}; - + drain: 'b -> 'a list * 'b}; -(* prompt *) - -val default_prompt = "> "; - -fun set_prompt prompt (Source {buffer, info, prompt = _, drain}) = - make_source buffer info prompt drain; +fun make_source buffer info drain = + Source {buffer = buffer, info = info, drain = drain}; (* get / unget *) -fun get (Source {buffer = [], info, prompt, drain}) = - let val (xs, info') = drain prompt info - in (xs, make_source [] info' prompt drain) end - | get (Source {buffer, info, prompt, drain}) = - (buffer, make_source [] info prompt drain); +fun get (Source {buffer = [], info, drain}) = + let val (xs, info') = drain info + in (xs, make_source [] info' drain) end + | get (Source {buffer, info, drain}) = (buffer, make_source [] info drain); -fun unget (xs, Source {buffer, info, prompt, drain}) = - make_source (xs @ buffer) info prompt drain; +fun unget (xs, Source {buffer, info, drain}) = make_source (xs @ buffer) info drain; (* variations on get *) -fun get_prompt prompt src = get (set_prompt prompt src); - fun get_single src = (case get src of ([], _) => NONE @@ -82,16 +66,16 @@ (* (map)filter *) -fun drain_map_filter f prompt src = +fun drain_map_filter f src = let - val (xs, src') = get_prompt prompt src; + val (xs, src') = get src; val xs' = map_filter f xs; in if null xs orelse not (null xs') then (xs', src') - else drain_map_filter f prompt src' + else drain_map_filter f src' end; -fun map_filter f src = make_source [] src default_prompt (drain_map_filter f); +fun map_filter f src = make_source [] src (drain_map_filter f); fun filter pred = map_filter (fn x => if pred x then SOME x else NONE); @@ -100,7 +84,7 @@ (* list source *) -fun of_list xs = make_source [] xs default_prompt (fn _ => fn xs => (xs, [])); +fun of_list xs = make_source [] xs (fn xs => (xs, [])); fun exhausted src = of_list (exhaust src); @@ -110,44 +94,23 @@ val of_string = of_list o raw_explode; fun of_string_limited limit str = - make_source [] (Substring.full str) default_prompt - (fn _ => fn s => + make_source [] (Substring.full str) + (fn s => let val (s1, s2) = Substring.splitAt (s, Int.min (Substring.size s, limit)); val cs = map String.str (Substring.explode s1); in (cs, s2) end); -(* stream source *) - -fun slurp_input instream = - let - fun slurp () = - (case TextIO.canInput (instream, 1) handle IO.Io _ => NONE of - NONE => [] - | SOME 0 => [] - | SOME _ => TextIO.input instream :: slurp ()); - in maps raw_explode (slurp ()) end; - -fun tty in_stream = make_source [] () default_prompt (fn prompt => fn () => - let val input = slurp_input in_stream in - if exists (fn c => c = "\n") input then (input, ()) - else - (case (Output.prompt prompt; TextIO.inputLine in_stream) of - SOME line => (input @ raw_explode line, ()) - | NONE => (input, ())) - end); - - (** cascade sources **) (* state-based *) -fun drain_source' stopper scan opt_recover prompt (state, src) = +fun drain_source' stopper scan opt_recover (state, src) = let - val drain = Scan.drain prompt get_prompt stopper; - val (xs, s) = get_prompt prompt src; + val drain = Scan.drain get stopper; + val (xs, s) = get src; val inp = ((state, xs), s); val ((ys, (state', xs')), src') = if null xs then (([], (state, [])), s) @@ -162,17 +125,16 @@ in (ys, (state', unget (xs', src'))) end; fun source' init_state stopper scan recover src = - make_source [] (init_state, src) default_prompt (drain_source' stopper scan recover); + make_source [] (init_state, src) (drain_source' stopper scan recover); (* non state-based *) -fun drain_source stopper scan opt_recover prompt = +fun drain_source stopper scan opt_recover = Scan.unlift (drain_source' stopper (Scan.lift scan) - (Option.map (fn (int, r) => (int, Scan.lift o r)) opt_recover) prompt); + (Option.map (fn (int, r) => (int, Scan.lift o r)) opt_recover)); fun source stopper scan recover src = - make_source [] src default_prompt (drain_source stopper scan recover); - + make_source [] src (drain_source stopper scan recover); end; diff -r e16712bb1d41 -r cc1e03929685 src/Pure/General/symbol.ML --- a/src/Pure/General/symbol.ML Fri Oct 31 17:01:54 2014 +0000 +++ b/src/Pure/General/symbol.ML Fri Oct 31 23:51:54 2014 +0100 @@ -19,9 +19,6 @@ val is_eof: symbol -> bool val not_eof: symbol -> bool val stopper: symbol Scan.stopper - val sync: symbol - val is_sync: symbol -> bool - val is_regular: symbol -> bool val is_malformed: symbol -> bool val malformed_msg: symbol -> string val is_ascii: symbol -> bool @@ -119,12 +116,6 @@ fun not_eof s = s <> eof; val stopper = Scan.stopper (K eof) is_eof; -(*Proof General legacy*) -val sync = "\\<^sync>"; -fun is_sync s = s = sync; - -fun is_regular s = not_eof s andalso s <> sync; - fun is_malformed s = String.isPrefix "\\<" s andalso not (String.isSuffix ">" s) orelse s = "\\<>" orelse s = "\\<^>"; diff -r e16712bb1d41 -r cc1e03929685 src/Pure/General/symbol_pos.ML --- a/src/Pure/General/symbol_pos.ML Fri Oct 31 17:01:54 2014 +0000 +++ b/src/Pure/General/symbol_pos.ML Fri Oct 31 23:51:54 2014 +0100 @@ -17,7 +17,6 @@ val is_eof: T -> bool val stopper: T Scan.stopper val !!! : Scan.message -> (T list -> 'a) -> T list -> 'a - val change_prompt: ('a -> 'b) -> 'a -> 'b val scan_pos: T list -> Position.T * T list val scan_string_q: string -> T list -> (Position.T * (T list * Position.T)) * T list val scan_string_qq: string -> T list -> (Position.T * (T list * Position.T)) * T list @@ -88,8 +87,6 @@ (case msg of NONE => "" | SOME m => "\n" ^ m ()); in Scan.!! err scan end; -fun change_prompt scan = Scan.prompt "# " scan; - fun $$ s = Scan.one (fn x => symbol x = s); fun ~$$ s = Scan.one (fn x => symbol x <> s); @@ -114,13 +111,13 @@ fun scan_str q err_prefix = $$$ "\\" |-- !!! (fn () => err_prefix ^ "bad escape character in string") ($$$ q || $$$ "\\" || char_code) || - Scan.one (fn (s, _) => s <> q andalso s <> "\\" andalso Symbol.is_regular s) >> single; + Scan.one (fn (s, _) => s <> q andalso s <> "\\" andalso Symbol.not_eof s) >> single; fun scan_strs q err_prefix = Scan.ahead ($$ q) |-- !!! (fn () => err_prefix ^ "unclosed string literal") ((scan_pos --| $$$ q) -- - (change_prompt ((Scan.repeat (scan_str q err_prefix) >> flat) -- ($$$ q |-- scan_pos)))); + ((Scan.repeat (scan_str q err_prefix) >> flat) -- ($$$ q |-- scan_pos))); fun recover_strs q = $$$ q @@@ (Scan.repeat (Scan.permissive (scan_str q "")) >> flat); @@ -167,14 +164,14 @@ Scan.repeat1 (Scan.depend (fn (d: int) => $$ "\\" >> pair (d + 1) || (if d > 0 then - Scan.one (fn (s, _) => s <> "\\" andalso Symbol.is_regular s) >> pair d || + Scan.one (fn (s, _) => s <> "\\" andalso Symbol.not_eof s) >> pair d || $$ "\\" >> pair (d - 1) else Scan.fail))); fun scan_cartouche err_prefix = Scan.ahead ($$ "\\") |-- !!! (fn () => err_prefix ^ "unclosed text cartouche") - (change_prompt (Scan.provide (fn d => d = 0) 0 scan_cartouche_depth)); + (Scan.provide (fn d => d = 0) 0 scan_cartouche_depth); val recover_cartouche = Scan.pass 0 scan_cartouche_depth; @@ -201,23 +198,21 @@ Scan.depend (fn (d: int) => $$$ "(" @@@ $$$ "*" >> pair (d + 1)) || Scan.depend (fn 0 => Scan.fail | d => $$$ "*" @@@ $$$ ")" >> pair (d - 1)) || Scan.lift ($$$ "*" --| Scan.ahead (~$$$ ")")) || - Scan.lift (Scan.one (fn (s, _) => s <> "*" andalso Symbol.is_regular s)) >> single; + Scan.lift (Scan.one (fn (s, _) => s <> "*" andalso Symbol.not_eof s)) >> single; val scan_cmts = Scan.pass 0 (Scan.repeat scan_cmt >> flat); -val scan_body = change_prompt scan_cmts; - in fun scan_comment err_prefix = Scan.ahead ($$ "(" -- $$ "*") |-- !!! (fn () => err_prefix ^ "unclosed comment") - ($$$ "(" @@@ $$$ "*" @@@ scan_body @@@ $$$ "*" @@@ $$$ ")"); + ($$$ "(" @@@ $$$ "*" @@@ scan_cmts @@@ $$$ "*" @@@ $$$ ")"); fun scan_comment_body err_prefix = Scan.ahead ($$ "(" -- $$ "*") |-- !!! (fn () => err_prefix ^ "unclosed comment") - ($$ "(" |-- $$ "*" |-- scan_body --| $$ "*" --| $$ ")"); + ($$ "(" |-- $$ "*" |-- scan_cmts --| $$ "*" --| $$ ")"); val recover_comment = $$$ "(" @@@ $$$ "*" @@@ scan_cmts; diff -r e16712bb1d41 -r cc1e03929685 src/Pure/General/url.ML --- a/src/Pure/General/url.ML Fri Oct 31 17:01:54 2014 +0000 +++ b/src/Pure/General/url.ML Fri Oct 31 23:51:54 2014 +0100 @@ -54,11 +54,11 @@ local val scan_host = - (Scan.many1 (fn s => s <> "/" andalso Symbol.is_regular s) >> implode) --| + (Scan.many1 (fn s => s <> "/" andalso Symbol.not_eof s) >> implode) --| Scan.ahead ($$ "/" || Scan.one Symbol.is_eof); -val scan_path = Scan.many Symbol.is_regular >> (Path.explode o implode); -val scan_path_root = Scan.many Symbol.is_regular >> (Path.explode o implode o cons "/"); +val scan_path = Scan.many Symbol.not_eof >> (Path.explode o implode); +val scan_path_root = Scan.many Symbol.not_eof >> (Path.explode o implode o cons "/"); val scan_url = Scan.unless (Scan.this_string "file:" || diff -r e16712bb1d41 -r cc1e03929685 src/Pure/Isar/calculation.ML --- a/src/Pure/Isar/calculation.ML Fri Oct 31 17:01:54 2014 +0000 +++ b/src/Pure/Isar/calculation.ML Fri Oct 31 23:51:54 2014 +0100 @@ -120,7 +120,7 @@ if int then Proof_Context.pretty_fact ctxt' (Proof_Context.full_name ctxt' (Binding.name calculationN), calc) - |> Pretty.string_of |> Output.urgent_message + |> Pretty.string_of |> writeln else (); in state' |> final ? (put_calculation NONE #> Proof.chain_facts calc) end; diff -r e16712bb1d41 -r cc1e03929685 src/Pure/Isar/isar_syn.ML --- a/src/Pure/Isar/isar_syn.ML Fri Oct 31 17:01:54 2014 +0000 +++ b/src/Pure/Isar/isar_syn.ML Fri Oct 31 23:51:54 2014 +0100 @@ -734,23 +734,6 @@ -(** nested commands **) - -val props_text = - Scan.optional Parse.properties [] -- Parse.position Parse.string - >> (fn (props, (str, pos)) => - (Position.of_properties (Position.default_properties pos props), str)); - -val _ = - Outer_Syntax.improper_command @{command_spec "Isabelle.command"} "evaluate nested Isabelle command" - (props_text :|-- (fn (pos, str) => - (case Outer_Syntax.parse (Outer_Syntax.get_syntax ()) pos str of - [tr] => Scan.succeed (K tr) - | _ => Scan.fail_with (K (fn () => "exactly one command expected"))) - handle ERROR msg => Scan.fail_with (K (fn () => msg)))); - - - (** diagnostic commands (for interactive mode only) **) val opt_modes = @@ -758,11 +741,6 @@ val opt_bang = Scan.optional (@{keyword "!"} >> K true) false; -val _ = (*Proof General legacy*) - Outer_Syntax.improper_command @{command_spec "pretty_setmargin"} - "change default margin for pretty printing" - (Parse.nat >> (fn n => Toplevel.imperative (fn () => Pretty.margin_default := n))); - val _ = Outer_Syntax.improper_command @{command_spec "help"} "retrieve outer syntax commands according to name patterns" @@ -890,13 +868,6 @@ (Scan.succeed Isar_Cmd.locale_deps); val _ = - Outer_Syntax.improper_command @{command_spec "print_binds"} - "print term bindings of proof context -- Proof General legacy" - (Scan.succeed (Toplevel.unknown_context o - Toplevel.keep - (Pretty.writeln_chunks o Proof_Context.pretty_term_bindings o Toplevel.context_of))); - -val _ = Outer_Syntax.improper_command @{command_spec "print_term_bindings"} "print term bindings of proof context" (Scan.succeed (Toplevel.unknown_context o @@ -948,110 +919,20 @@ (Scan.succeed (Toplevel.unknown_theory o Toplevel.keep (Code.print_codesetup o Toplevel.theory_of))); - - -(** system commands (for interactive mode only) **) - -val _ = - Outer_Syntax.improper_command @{command_spec "use_thy"} "use theory file" - (Parse.position Parse.name >> - (fn name => Toplevel.imperative (fn () => Thy_Info.use_thy name))); - -val _ = - Outer_Syntax.improper_command @{command_spec "remove_thy"} "remove theory from loader database" - (Parse.name >> (fn name => Toplevel.imperative (fn () => Thy_Info.remove_thy name))); - -val _ = - Outer_Syntax.improper_command @{command_spec "kill_thy"} - "kill theory -- try to remove from loader database" - (Parse.name >> (fn name => Toplevel.imperative (fn () => Thy_Info.kill_thy name))); - -val _ = (*partial Proof General legacy*) - Outer_Syntax.improper_command @{command_spec "display_drafts"} - "display raw source files with symbols" - (Scan.repeat1 Parse.path >> (fn names => - Toplevel.imperative (fn () => ignore (Present.display_drafts (map Path.explode names))))); - val _ = Outer_Syntax.improper_command @{command_spec "print_state"} "print current proof state (if present)" (opt_modes >> (fn modes => Toplevel.keep (Print_Mode.with_modes modes Toplevel.print_state))); -val _ = (*Proof General legacy, e.g. for ProofGeneral-3.7.x*) - Outer_Syntax.improper_command @{command_spec "pr"} "print current proof state (if present)" - (opt_modes -- Scan.option Parse.nat >> (fn (modes, limit) => - Toplevel.keep (fn state => - (if Isabelle_Process.is_active () then error "Illegal TTY command" else (); - case limit of NONE => () | SOME n => Options.default_put_int @{system_option goals_limit} n; - Toplevel.quiet := false; - Print_Mode.with_modes modes Toplevel.print_state state)))); - -val _ = (*Proof General legacy*) - Outer_Syntax.improper_command @{command_spec "disable_pr"} - "disable printing of toplevel state" - (Scan.succeed (Toplevel.imperative (fn () => Toplevel.quiet := true))); - -val _ = (*Proof General legacy*) - Outer_Syntax.improper_command @{command_spec "enable_pr"} - "enable printing of toplevel state" - (Scan.succeed (Toplevel.imperative (fn () => Toplevel.quiet := false))); - -val _ = - Outer_Syntax.improper_command @{command_spec "commit"} - "commit current session to ML session image" - (Parse.opt_unit >> K (Toplevel.imperative Secure.commit)); - -val _ = - Outer_Syntax.improper_command @{command_spec "quit"} "quit Isabelle process" - (Parse.opt_unit >> (K (Toplevel.imperative quit))); - -val _ = - Outer_Syntax.improper_command @{command_spec "exit"} "exit Isar loop" - (Scan.succeed - (Toplevel.keep (fn state => - (Context.set_thread_data (try Toplevel.generic_theory_of state); - raise Runtime.TERMINATE)))); - val _ = Outer_Syntax.improper_command @{command_spec "welcome"} "print welcome message" (Scan.succeed (Toplevel.imperative (writeln o Session.welcome))); - - -(** raw Isar read-eval-print loop **) - val _ = - Outer_Syntax.improper_command @{command_spec "init_toplevel"} "init toplevel point-of-interest" - (Scan.succeed (Toplevel.imperative Isar.init)); - -val _ = - Outer_Syntax.improper_command @{command_spec "linear_undo"} "undo commands" - (Scan.optional Parse.nat 1 >> - (fn n => Toplevel.imperative (fn () => Isar.linear_undo n))); - -val _ = - Outer_Syntax.improper_command @{command_spec "undo"} "undo commands (skipping closed proofs)" - (Scan.optional Parse.nat 1 >> - (fn n => Toplevel.imperative (fn () => Isar.undo n))); - -val _ = - Outer_Syntax.improper_command @{command_spec "undos_proof"} - "undo commands (skipping closed proofs)" - (Scan.optional Parse.nat 1 >> (fn n => - Toplevel.keep (fn state => - if Toplevel.is_proof state then (Isar.undo n; Isar.print ()) else raise Toplevel.UNDEF))); - -val _ = - Outer_Syntax.improper_command @{command_spec "cannot_undo"} - "partial undo -- Proof General legacy" - (Parse.name >> - (fn "end" => Toplevel.imperative (fn () => Isar.undo 1) - | txt => Toplevel.imperative (fn () => error ("Cannot undo " ^ quote txt)))); - -val _ = - Outer_Syntax.improper_command @{command_spec "kill"} - "kill partial proof or theory development" - (Scan.succeed (Toplevel.imperative Isar.kill)); + Outer_Syntax.improper_command @{command_spec "display_drafts"} + "display raw source files with symbols" + (Scan.repeat1 Parse.path >> (fn names => + Toplevel.imperative (fn () => ignore (Present.display_drafts (map Path.explode names))))); diff -r e16712bb1d41 -r cc1e03929685 src/Pure/Isar/keyword.ML --- a/src/Pure/Isar/keyword.ML Fri Oct 31 17:01:54 2014 +0000 +++ b/src/Pure/Isar/keyword.ML Fri Oct 31 23:51:54 2014 +0100 @@ -9,7 +9,6 @@ type T val kind_of: T -> string val kind_files_of: T -> string * string list - val control: T val diag: T val thy_begin: T val thy_end: T @@ -56,8 +55,6 @@ val dest: unit -> string list * string list val define: string * T option -> unit val is_diag: string -> bool - val is_control: string -> bool - val is_regular: string -> bool val is_heading: string -> bool val is_theory_begin: string -> bool val is_theory_load: string -> bool @@ -92,7 +89,6 @@ (* kinds *) -val control = kind "control"; val diag = kind "diag"; val thy_begin = kind "thy_begin"; val thy_end = kind "thy_end"; @@ -124,7 +120,7 @@ val prf_script = kind "prf_script"; val kinds = - [control, diag, thy_begin, thy_end, thy_heading1, thy_heading2, thy_heading3, thy_heading4, + [diag, thy_begin, thy_end, thy_heading1, thy_heading2, thy_heading3, thy_heading4, thy_load, thy_decl, thy_decl_block, thy_goal, qed, qed_script, qed_block, qed_global, prf_heading2, prf_heading3, prf_heading4, prf_goal, prf_block, prf_open, prf_close, prf_chain, prf_decl, prf_asm, prf_asm_goal, prf_asm_goal_script, prf_script]; @@ -238,8 +234,6 @@ end; val is_diag = command_category [diag]; -val is_control = command_category [control]; -val is_regular = not o command_category [diag, control]; val is_heading = command_category [thy_heading1, thy_heading2, thy_heading3, thy_heading4, diff -r e16712bb1d41 -r cc1e03929685 src/Pure/Isar/keyword.scala --- a/src/Pure/Isar/keyword.scala Fri Oct 31 17:01:54 2014 +0000 +++ b/src/Pure/Isar/keyword.scala Fri Oct 31 23:51:54 2014 +0100 @@ -12,7 +12,6 @@ /* kinds */ val MINOR = "minor" - val CONTROL = "control" val DIAG = "diag" val THY_BEGIN = "thy_begin" val THY_END = "thy_end" @@ -46,7 +45,6 @@ /* categories */ val diag = Set(DIAG) - val control = Set(CONTROL) val heading = Set(THY_HEADING1, THY_HEADING2, THY_HEADING3, THY_HEADING4, PRF_HEADING2, PRF_HEADING3, PRF_HEADING4) diff -r e16712bb1d41 -r cc1e03929685 src/Pure/Isar/outer_syntax.ML --- a/src/Pure/Isar/outer_syntax.ML Fri Oct 31 17:01:54 2014 +0000 +++ b/src/Pure/Isar/outer_syntax.ML Fri Oct 31 23:51:54 2014 +0100 @@ -35,8 +35,6 @@ val parse: (Scan.lexicon * Scan.lexicon) * outer_syntax -> Position.T -> string -> Toplevel.transition list val parse_spans: Token.T list -> Command_Span.span list - type isar - val isar: TextIO.instream -> bool -> isar val side_comments: Token.T list -> Token.T list val command_reports: outer_syntax -> Token.T -> Position.report_text list val read_spans: outer_syntax -> Token.T list -> Toplevel.transition list @@ -77,14 +75,12 @@ local fun terminate false = Scan.succeed () - | terminate true = - Parse.group (fn () => "end of input") - (Scan.option Parse.sync -- Parse.semicolon >> K ()); + | terminate true = Parse.group (fn () => "end of input") (Parse.semicolon >> K ()); fun body cmd (name, _) = (case cmd name of SOME (Command {int_only, parse, ...}) => - Parse.!!! (Scan.prompt (name ^ "# ") (Parse.tags |-- parse >> pair int_only)) + Parse.!!! (Parse.tags |-- parse >> pair int_only) | NONE => Scan.succeed (false, Toplevel.imperative (fn () => error ("Bad parser for outer syntax command " ^ quote name)))); @@ -93,7 +89,6 @@ fun parse_command do_terminate cmd = Parse.semicolon >> K NONE || - Parse.sync >> K NONE || (Parse.position Parse.command :-- body cmd) --| terminate do_terminate >> (fn ((name, pos), (int_only, f)) => SOME (Toplevel.empty |> Toplevel.name name |> Toplevel.position pos |> @@ -184,8 +179,6 @@ | missing => error ("Missing outer syntax command(s) " ^ commas_quote missing)) end; -fun lookup_commands_dynamic () = lookup_commands (! global_outer_syntax); - fun command (spec, pos) comment parse = add_command spec (new_command comment NONE false parse pos); @@ -238,10 +231,8 @@ fun toplevel_source term do_recover cmd src = let - val no_terminator = - Scan.unless Parse.semicolon (Scan.one (Token.not_sync andf Token.not_eof)); - fun recover int = - (int, fn _ => Scan.prompt "recover# " (Scan.repeat no_terminator) >> K [NONE]); + val no_terminator = Scan.unless Parse.semicolon (Scan.one Token.not_eof); + fun recover int = (int, fn _ => Scan.repeat no_terminator >> K [NONE]); in src |> Token.source_proper @@ -303,24 +294,6 @@ end; -(* interactive source of toplevel transformers *) - -type isar = - (Toplevel.transition, (Toplevel.transition option, - (Token.T, (Token.T option, (Token.T, (Token.T, - (Symbol_Pos.T, - Position.T * (Symbol.symbol, (Symbol.symbol, (string, unit) Source.source) Source.source) - Source.source) Source.source) Source.source) Source.source) - Source.source) Source.source) Source.source) Source.source; - -fun isar in_stream term : isar = - Source.tty in_stream - |> Symbol.source - |> Source.map_filter (fn "\<^newline>" => SOME "\n" | s => SOME s) (*Proof General legacy*) - |> Token.source {do_recover = SOME true} Keyword.get_lexicons Position.none - |> toplevel_source term (SOME true) lookup_commands_dynamic; - - (* side-comments *) fun cmts (t1 :: t2 :: toks) = diff -r e16712bb1d41 -r cc1e03929685 src/Pure/Isar/outer_syntax.scala --- a/src/Pure/Isar/outer_syntax.scala Fri Oct 31 17:01:54 2014 +0000 +++ b/src/Pure/Isar/outer_syntax.scala Fri Oct 31 23:51:54 2014 +0100 @@ -129,7 +129,7 @@ val keywords1 = keywords + (name -> kind) val lexicon1 = lexicon + name val completion1 = - if (Keyword.control(kind._1) || replace == Some("")) completion + if (replace == Some("")) completion else completion + (name, replace getOrElse name) new Outer_Syntax(keywords1, lexicon1, completion1, language_context, true) } diff -r e16712bb1d41 -r cc1e03929685 src/Pure/Isar/parse.ML --- a/src/Pure/Isar/parse.ML Fri Oct 31 17:01:54 2014 +0000 +++ b/src/Pure/Isar/parse.ML Fri Oct 31 23:51:54 2014 +0100 @@ -32,7 +32,6 @@ val alt_string: string parser val verbatim: string parser val cartouche: string parser - val sync: string parser val eof: string parser val command_name: string -> string parser val keyword_with: (string -> bool) -> string parser @@ -196,7 +195,6 @@ val alt_string = kind Token.AltString; val verbatim = kind Token.Verbatim; val cartouche = kind Token.Cartouche; -val sync = kind Token.Sync; val eof = kind Token.EOF; fun command_name x = diff -r e16712bb1d41 -r cc1e03929685 src/Pure/Isar/runtime.ML --- a/src/Pure/Isar/runtime.ML Fri Oct 31 17:01:54 2014 +0000 +++ b/src/Pure/Isar/runtime.ML Fri Oct 31 23:51:54 2014 +0100 @@ -172,7 +172,7 @@ (fn () => debugging NONE body () handle exn => if Exn.is_interrupt exn then () - else Output.urgent_message ("## INTERNAL ERROR ##\n" ^ exn_message exn), + else writeln ("## INTERNAL ERROR ##\n" ^ exn_message exn), Simple_Thread.attributes interrupts); end; diff -r e16712bb1d41 -r cc1e03929685 src/Pure/Isar/specification.ML --- a/src/Pure/Isar/specification.ML Fri Oct 31 17:01:54 2014 +0000 +++ b/src/Pure/Isar/specification.ML Fri Oct 31 23:51:54 2014 +0100 @@ -74,7 +74,6 @@ (thm list list -> local_theory -> local_theory) -> Attrib.binding -> (xstring * Position.T) list -> Element.context list -> Element.statement -> bool -> local_theory -> Proof.state - val add_theorem_hook: (bool -> Proof.state -> Proof.state) -> Context.generic -> Context.generic end; structure Specification: SPECIFICATION = @@ -372,14 +371,6 @@ #2 #> pair ths); in ((more_atts, prems, stmt, SOME facts), goal_ctxt) end); -structure Theorem_Hook = Generic_Data -( - type T = ((bool -> Proof.state -> Proof.state) * stamp) list; - val empty = []; - val extend = I; - fun merge data : T = Library.merge (eq_snd op =) data; -); - fun gen_theorem schematic bundle_includes prep_att prep_stmt kind before_qed after_qed (name, raw_atts) raw_includes raw_elems raw_concl int lthy = let @@ -419,7 +410,6 @@ |> (case facts of NONE => I | SOME ths => Proof.refine_insert ths) |> tap (fn state => not schematic andalso Proof.schematic_goal state andalso error "Illegal schematic goal statement") - |> fold_rev (fn (f, _) => f int) (Theorem_Hook.get (Context.Proof goal_ctxt)) end; in @@ -434,8 +424,6 @@ val schematic_theorem_cmd = gen_theorem true Bundle.includes_cmd Attrib.check_src Expression.read_statement; -fun add_theorem_hook f = Theorem_Hook.map (cons (f, stamp ())); - end; end; diff -r e16712bb1d41 -r cc1e03929685 src/Pure/Isar/token.ML --- a/src/Pure/Isar/token.ML Fri Oct 31 17:01:54 2014 +0000 +++ b/src/Pure/Isar/token.ML Fri Oct 31 23:51:54 2014 +0100 @@ -9,7 +9,7 @@ datatype kind = Command | Keyword | Ident | LongIdent | SymIdent | Var | TypeIdent | TypeVar | Nat | Float | String | AltString | Verbatim | Cartouche | Space | Comment | InternalValue | - Error of string | Sync | EOF + Error of string | EOF val str_of_kind: kind -> string type file = {src_path: Path.T, lines: string list, digest: SHA1.digest, pos: Position.T} type T @@ -35,7 +35,6 @@ val eof: T val is_eof: T -> bool val not_eof: T -> bool - val not_sync: T -> bool val stopper: T Scan.stopper val kind_of: T -> kind val is_kind: kind -> T -> bool @@ -104,7 +103,7 @@ datatype kind = Command | Keyword | Ident | LongIdent | SymIdent | Var | TypeIdent | TypeVar | Nat | Float | String | AltString | Verbatim | Cartouche | Space | Comment | InternalValue | - Error of string | Sync | EOF; + Error of string | EOF; val str_of_kind = fn Command => "command" @@ -125,7 +124,6 @@ | Comment => "comment text" | InternalValue => "internal value" | Error _ => "bad input" - | Sync => "sync marker" | EOF => "end-of-input"; val delimited_kind = member (op =) [String, AltString, Verbatim, Cartouche, Comment]; @@ -201,7 +199,7 @@ in (Src {name = (name, pos), args = args, output_info = SOME (kind, markup)}, x) end; -(* control tokens *) +(* stopper *) fun mk_eof pos = Token (("", (pos, Position.none)), (EOF, ""), Slot); val eof = mk_eof Position.none; @@ -211,9 +209,6 @@ val not_eof = not o is_eof; -fun not_sync (Token (_, (Sync, _), _)) = false - | not_sync _ = true; - val stopper = Scan.stopper (fn [] => eof | toks => mk_eof (end_pos_of (List.last toks))) is_eof; @@ -305,8 +300,7 @@ | Comment => (Markup.comment, "") | InternalValue => (Markup.empty, "") | Error msg => (Markup.bad, msg) - | Sync => (Markup.control, "") - | EOF => (Markup.control, ""); + | EOF => (Markup.empty, ""); in @@ -339,7 +333,6 @@ | Verbatim => enclose "{*" "*}" x | Cartouche => cartouche x | Comment => enclose "(*" "*)" x - | Sync => "" | EOF => "" | _ => x); @@ -493,14 +486,13 @@ val scan_verb = $$$ "*" --| Scan.ahead (~$$ "}") || - Scan.one (fn (s, _) => s <> "*" andalso Symbol.is_regular s) >> single; + Scan.one (fn (s, _) => s <> "*" andalso Symbol.not_eof s) >> single; val scan_verbatim = Scan.ahead ($$ "{" -- $$ "*") |-- !!! "unclosed verbatim text" ((Symbol_Pos.scan_pos --| $$ "{" --| $$ "*") -- - Symbol_Pos.change_prompt - ((Scan.repeat scan_verb >> flat) -- ($$ "*" |-- $$ "}" |-- Symbol_Pos.scan_pos))); + ((Scan.repeat scan_verb >> flat) -- ($$ "*" |-- $$ "}" |-- Symbol_Pos.scan_pos))); val recover_verbatim = $$$ "{" @@@ $$$ "*" @@@ (Scan.repeat scan_verb >> flat); @@ -550,7 +542,6 @@ scan_cartouche >> token_range Cartouche || scan_comment >> token_range Comment || scan_space >> token Space || - Scan.one (Symbol.is_sync o Symbol_Pos.symbol) >> (token Sync o single) || (Scan.max token_leq (Scan.max token_leq (Scan.literal lex2 >> pair Command) @@ -570,7 +561,7 @@ recover_verbatim || Symbol_Pos.recover_cartouche || Symbol_Pos.recover_comment || - Scan.one (Symbol.is_regular o Symbol_Pos.symbol) >> single) + Scan.one (Symbol.not_eof o Symbol_Pos.symbol) >> single) >> (single o token (Error msg)); in diff -r e16712bb1d41 -r cc1e03929685 src/Pure/Isar/toplevel.ML --- a/src/Pure/Isar/toplevel.ML Fri Oct 31 17:01:54 2014 +0000 +++ b/src/Pure/Isar/toplevel.ML Fri Oct 31 23:51:54 2014 +0100 @@ -26,9 +26,6 @@ val pretty_state: state -> Pretty.T list val print_state: state -> unit val pretty_abstract: state -> Pretty.T - val quiet: bool Unsynchronized.ref - val interact: bool Unsynchronized.ref - val timing: bool Unsynchronized.ref val profiling: int Unsynchronized.ref type transition val empty: transition @@ -213,9 +210,6 @@ (** toplevel transitions **) -val quiet = Unsynchronized.ref false; (*Proof General legacy*) -val interact = Unsynchronized.ref false; (*Proof General legacy*) -val timing = Unsynchronized.ref false; (*Proof General legacy*) val profiling = Unsynchronized.ref 0; @@ -528,12 +522,10 @@ (fn Proof (prf, x) => Proof (f prf, x) | _ => raise UNDEF)); -(*Proof General legacy*) fun skip_proof f = transaction (fn _ => (fn Skipped_Proof (h, x) => Skipped_Proof (f h, x) | _ => raise UNDEF)); -(*Proof General legacy*) fun skip_proof_to_theory pred = transaction (fn _ => (fn Skipped_Proof (d, (gthy, _)) => if pred d then Theory (gthy, NONE) else raise UNDEF | _ => raise UNDEF)); @@ -580,10 +572,6 @@ val (result, opt_err) = state |> (apply_trans int trans |> ! profiling > 0 ? profile (! profiling)); - val _ = - if int andalso not (! quiet) andalso Keyword.is_printed name - then print_state result else (); - val timing_result = Timing.result timing_start; val timing_props = Markup.command_timing :: (Markup.nameN, name_of tr) :: Position.properties_of (pos_of tr); @@ -627,7 +615,7 @@ if Exn.is_interrupt exn then reraise exn else raise Runtime.EXCURSION_FAIL (exn, info) | NONE => raise Runtime.EXCURSION_FAIL (Runtime.TERMINATE, at_command tr)); -fun command tr = command_exception (! interact) tr; +val command = command_exception false; (* reset state *) diff -r e16712bb1d41 -r cc1e03929685 src/Pure/ML/ml_lex.ML --- a/src/Pure/ML/ml_lex.ML Fri Oct 31 17:01:54 2014 +0000 +++ b/src/Pure/ML/ml_lex.ML Fri Oct 31 23:51:54 2014 +0100 @@ -73,7 +73,7 @@ fun end_pos_of (Token ((_, pos), _)) = pos; -(* control tokens *) +(* stopper *) fun mk_eof pos = Token ((pos, Position.none), (EOF, "")); val eof = mk_eof Position.none; @@ -236,7 +236,7 @@ Scan.one (Symbol.is_ascii_digit o Symbol_Pos.symbol) >> (fn ((a, b), c) => [a, b, c]); val scan_str = - Scan.one (fn (s, _) => Symbol.is_regular s andalso s <> "\"" andalso s <> "\\" andalso + Scan.one (fn (s, _) => Symbol.not_eof s andalso s <> "\"" andalso s <> "\\" andalso (not (Symbol.is_char s) orelse Symbol.is_printable s)) >> single || $$$ "\\" @@@ !!! "bad escape character in string" scan_escape; diff -r e16712bb1d41 -r cc1e03929685 src/Pure/PIDE/command.ML --- a/src/Pure/PIDE/command.ML Fri Oct 31 17:01:54 2014 +0000 +++ b/src/Pure/PIDE/command.ML Fri Oct 31 23:51:54 2014 +0100 @@ -162,10 +162,7 @@ if is_malformed then Toplevel.malformed pos "Malformed command syntax" else (case Outer_Syntax.read_spans outer_syntax (resolve_files master_dir blobs span) of - [tr] => - if Keyword.is_control (Toplevel.name_of tr) then - Toplevel.malformed pos "Illegal control command" - else Toplevel.modify_init init tr + [tr] => Toplevel.modify_init init tr | [] => Toplevel.ignored (#1 (Token.range_of span)) | _ => Toplevel.malformed (#1 proper_range) "Exactly one command expected") handle ERROR msg => Toplevel.malformed (#1 proper_range) msg diff -r e16712bb1d41 -r cc1e03929685 src/Pure/PIDE/markup.ML --- a/src/Pure/PIDE/markup.ML Fri Oct 31 17:01:54 2014 +0000 +++ b/src/Pure/PIDE/markup.ML Fri Oct 31 23:51:54 2014 +0100 @@ -118,7 +118,6 @@ val verbatimN: string val verbatim: T val cartoucheN: string val cartouche: T val commentN: string val comment: T - val controlN: string val control: T val tokenN: string val token: bool -> Properties.T -> T val keyword1N: string val keyword1: T val keyword2N: string val keyword2: T @@ -162,7 +161,6 @@ val systemN: string val protocolN: string val legacyN: string val legacy: T - val promptN: string val prompt: T val reportN: string val report: T val no_reportN: string val no_report: T val badN: string val bad: T @@ -465,7 +463,6 @@ val (verbatimN, verbatim) = markup_elem "verbatim"; val (cartoucheN, cartouche) = markup_elem "cartouche"; val (commentN, comment) = markup_elem "comment"; -val (controlN, control) = markup_elem "control"; val tokenN = "token"; fun token delimited props = (tokenN, (delimitedN, print_bool delimited) :: props); @@ -547,7 +544,6 @@ val protocolN = "protocol"; val (legacyN, legacy) = markup_elem "legacy"; -val (promptN, prompt) = markup_elem "prompt"; val (reportN, report) = markup_elem "report"; val (no_reportN, no_report) = markup_elem "no_report"; diff -r e16712bb1d41 -r cc1e03929685 src/Pure/PIDE/markup.scala --- a/src/Pure/PIDE/markup.scala Fri Oct 31 17:01:54 2014 +0000 +++ b/src/Pure/PIDE/markup.scala Fri Oct 31 23:51:54 2014 +0100 @@ -264,7 +264,6 @@ val VERBATIM = "verbatim" val CARTOUCHE = "cartouche" val COMMENT = "comment" - val CONTROL = "control" /* timing */ diff -r e16712bb1d41 -r cc1e03929685 src/Pure/PIDE/resources.ML --- a/src/Pure/PIDE/resources.ML Fri Oct 31 17:01:54 2014 +0000 +++ b/src/Pure/PIDE/resources.ML Fri Oct 31 23:51:54 2014 +0100 @@ -15,7 +15,6 @@ val parse_files: string -> (theory -> Token.file list) parser val provide: Path.T * SHA1.digest -> theory -> theory val provide_parse_files: string -> (theory -> Token.file list * theory) parser - val loaded_files: theory -> Path.T list val loaded_files_current: theory -> bool val begin_theory: Path.T -> Thy_Header.header -> theory list -> theory val load_thy: bool -> (Toplevel.transition -> Time.time option) -> int -> Path.T -> @@ -116,11 +115,6 @@ NONE => false | SOME ((_, id'), _) => id = id')); -(*Proof General legacy*) -fun loaded_files thy = - let val {master_dir, provided, ...} = Files.get thy - in map (File.full_path master_dir o #1) provided end; - (* load theory *) @@ -151,8 +145,6 @@ fun load_thy document last_timing update_time master_dir header text_pos text parents = let - val time = ! Toplevel.timing; - val {name = (name, _), ...} = header; val _ = Thy_Header.define_keywords header; @@ -166,10 +158,9 @@ |> Present.begin_theory update_time (fn () => HTML.html_mode (implode o map Thy_Syntax.present_span) spans); - val _ = if time then writeln ("\n**** Starting theory " ^ quote name ^ " ****") else (); val (results, thy) = - cond_timeit time "" (fn () => excursion master_dir last_timing init elements); - val _ = if time then writeln ("**** Finished theory " ^ quote name ^ " ****\n") else (); + cond_timeit true ("theory " ^ quote name) + (fn () => excursion master_dir last_timing init elements); fun present () = let diff -r e16712bb1d41 -r cc1e03929685 src/Pure/PIDE/xml.ML --- a/src/Pure/PIDE/xml.ML Fri Oct 31 17:01:54 2014 +0000 +++ b/src/Pure/PIDE/xml.ML Fri Oct 31 23:51:54 2014 +0100 @@ -192,8 +192,8 @@ val blanks = Scan.many Symbol.is_blank; val special = $$ "&" ^^ (parse_name >> implode) ^^ $$ ";" >> decode; -val regular = Scan.one Symbol.is_regular; -fun regular_except x = Scan.one (fn c => Symbol.is_regular c andalso c <> x); +val regular = Scan.one Symbol.not_eof; +fun regular_except x = Scan.one (fn c => Symbol.not_eof c andalso c <> x); val parse_chars = Scan.repeat1 (special || regular_except "<") >> implode; diff -r e16712bb1d41 -r cc1e03929685 src/Pure/Proof/extraction.ML --- a/src/Pure/Proof/extraction.ML Fri Oct 31 17:01:54 2014 +0000 +++ b/src/Pure/Proof/extraction.ML Fri Oct 31 23:51:54 2014 +0100 @@ -121,7 +121,7 @@ fun extr_name s vs = Long_Name.append "extr" (space_implode "_" (s :: vs)); fun corr_name s vs = extr_name s vs ^ "_correctness"; -fun msg d s = Output.urgent_message (Pretty.spaces d ^ s); +fun msg d s = writeln (Pretty.spaces d ^ s); fun vars_of t = map Var (rev (Term.add_vars t [])); fun frees_of t = map Free (rev (Term.add_frees t [])); diff -r e16712bb1d41 -r cc1e03929685 src/Pure/Pure.thy --- a/src/Pure/Pure.thy Fri Oct 31 17:01:54 2014 +0000 +++ b/src/Pure/Pure.thy Fri Oct 31 23:51:54 2014 +0100 @@ -79,30 +79,23 @@ and "also" "moreover" :: prf_decl % "proof" and "finally" "ultimately" :: prf_chain % "proof" and "back" :: prf_script % "proof" - and "Isabelle.command" :: control and "help" "print_commands" "print_options" "print_context" "print_theory" "print_syntax" "print_abbrevs" "print_defn_rules" "print_theorems" "print_locales" "print_classes" "print_locale" "print_interps" "print_dependencies" "print_attributes" "print_simpset" "print_rules" "print_trans_rules" "print_methods" "print_antiquotations" "print_ML_antiquotations" "thy_deps" - "locale_deps" "class_deps" "thm_deps" "print_binds" "print_term_bindings" + "locale_deps" "class_deps" "thm_deps" "print_term_bindings" "print_facts" "print_cases" "print_statement" "thm" "prf" "full_prf" "prop" "term" "typ" "print_codesetup" "unused_thms" :: diag - and "use_thy" "remove_thy" "kill_thy" :: control - and "display_drafts" "print_state" "pr" :: diag - and "pretty_setmargin" "disable_pr" "enable_pr" "commit" "quit" "exit" :: control + and "display_drafts" "print_state" :: diag and "welcome" :: diag - and "init_toplevel" "linear_undo" "undo" "undos_proof" "cannot_undo" "kill" :: control and "end" :: thy_end % "theory" and "realizers" :: thy_decl == "" and "realizability" :: thy_decl == "" 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 +110,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 e16712bb1d41 -r cc1e03929685 src/Pure/ROOT --- a/src/Pure/ROOT Fri Oct 31 17:01:54 2014 +0000 +++ b/src/Pure/ROOT Fri Oct 31 23:51:54 2014 +0100 @@ -196,7 +196,6 @@ "System/invoke_scala.ML" "System/isabelle_process.ML" "System/isabelle_system.ML" - "System/isar.ML" "System/message_channel.ML" "System/options.ML" "System/system_channel.ML" @@ -211,7 +210,6 @@ "Tools/build.ML" "Tools/named_thms.ML" "Tools/plugin.ML" - "Tools/proof_general.ML" "assumption.ML" "axclass.ML" "config.ML" diff -r e16712bb1d41 -r cc1e03929685 src/Pure/ROOT.ML --- a/src/Pure/ROOT.ML Fri Oct 31 17:01:54 2014 +0000 +++ b/src/Pure/ROOT.ML Fri Oct 31 23:51:54 2014 +0100 @@ -327,14 +327,12 @@ 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!*) diff -r e16712bb1d41 -r cc1e03929685 src/Pure/Syntax/lexicon.ML --- a/src/Pure/Syntax/lexicon.ML Fri Oct 31 17:01:54 2014 +0000 +++ b/src/Pure/Syntax/lexicon.ML Fri Oct 31 23:51:54 2014 +0100 @@ -230,7 +230,7 @@ val scan_chr = $$ "\\" |-- $$$ "'" || Scan.one - ((fn s => s <> "\\" andalso s <> "'" andalso Symbol.is_regular s) o + ((fn s => s <> "\\" andalso s <> "'" andalso Symbol.not_eof s) o Symbol_Pos.symbol) >> single || $$$ "'" --| Scan.ahead (~$$ "'"); @@ -339,7 +339,7 @@ val scan = $$ "?" |-- scan_indexname --| Scan.ahead (Scan.one Symbol_Pos.is_eof) >> Syntax.var || - Scan.many (Symbol.is_regular o Symbol_Pos.symbol) + Scan.many (Symbol.not_eof o Symbol_Pos.symbol) >> (Syntax.free o implode o map Symbol_Pos.symbol); in the (Scan.read Symbol_Pos.stopper scan (Symbol_Pos.explode (str, Position.none))) end; diff -r e16712bb1d41 -r cc1e03929685 src/Pure/Syntax/syntax_ext.ML --- a/src/Pure/Syntax/syntax_ext.ML Fri Oct 31 17:01:54 2014 +0000 +++ b/src/Pure/Syntax/syntax_ext.ML Fri Oct 31 23:51:54 2014 +0100 @@ -143,8 +143,8 @@ val is_meta = member (op =) ["(", ")", "/", "_", "\\"]; val scan_delim_char = - $$ "'" |-- Scan.one ((not o Symbol.is_blank) andf Symbol.is_regular) || - Scan.one ((not o is_meta) andf (not o Symbol.is_blank) andf Symbol.is_regular); + $$ "'" |-- Scan.one ((not o Symbol.is_blank) andf Symbol.not_eof) || + Scan.one ((not o is_meta) andf (not o Symbol.is_blank) andf Symbol.not_eof); fun read_int ["0", "0"] = ~1 | read_int cs = #1 (Library.read_int cs); diff -r e16712bb1d41 -r cc1e03929685 src/Pure/System/isabelle_process.ML --- a/src/Pure/System/isabelle_process.ML Fri Oct 31 17:01:54 2014 +0000 +++ b/src/Pure/System/isabelle_process.ML Fri Oct 31 23:51:54 2014 +0100 @@ -126,8 +126,6 @@ (fn (i, s) => standard_message (Markup.serial_properties i) Markup.errorN s); Output.system_message_fn := message Markup.systemN []; Output.protocol_message_fn := message Markup.protocolN; - Output.urgent_message_fn := ! Output.writeln_fn; - Output.prompt_fn := ignore; message Markup.initN [] [Session.welcome ()]; msg_channel end; @@ -205,7 +203,7 @@ val channel = rendezvous (); val msg_channel = init_channels channel; val _ = Session.init_protocol_handlers (); - val _ = (loop |> Unsynchronized.setmp Toplevel.quiet true) channel; + val _ = loop channel; in Message_Channel.shutdown msg_channel end); fun init_fifos fifo1 fifo2 = init (fn () => System_Channel.fifo_rendezvous fifo1 fifo2); diff -r e16712bb1d41 -r cc1e03929685 src/Pure/System/isar.ML --- a/src/Pure/System/isar.ML Fri Oct 31 17:01:54 2014 +0000 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,174 +0,0 @@ -(* Title: Pure/System/isar.ML - Author: Makarius - -Global state of the raw Isar read-eval-print loop. -*) - -signature ISAR = -sig - val init: unit -> unit - val exn: unit -> (exn * string) option - val state: unit -> Toplevel.state - val goal: unit -> {context: Proof.context, facts: thm list, goal: thm} - val print: unit -> unit - val >> : Toplevel.transition -> bool - val >>> : Toplevel.transition list -> unit - val linear_undo: int -> unit - val undo: int -> unit - val kill: unit -> unit - val kill_proof: unit -> unit - val crashes: exn list Synchronized.var - val toplevel_loop: TextIO.instream -> - {init: bool, welcome: bool, sync: bool, secure: bool} -> unit - val loop: unit -> unit - val main: unit -> unit -end; - -structure Isar: ISAR = -struct - - -(** TTY model -- SINGLE-THREADED! **) - -(* the global state *) - -type history = (Toplevel.state * Toplevel.transition) list; - (*previous state, state transition -- regular commands only*) - -local - val global_history = Unsynchronized.ref ([]: history); - val global_state = Unsynchronized.ref Toplevel.toplevel; - val global_exn = Unsynchronized.ref (NONE: (exn * string) option); -in - -fun edit_history count f = NAMED_CRITICAL "Isar" (fn () => - let - fun edit 0 (st, hist) = (global_history := hist; global_state := st; global_exn := NONE) - | edit n (st, hist) = edit (n - 1) (f st hist); - in edit count (! global_state, ! global_history) end); - -fun state () = ! global_state; - -fun exn () = ! global_exn; -fun set_exn exn = global_exn := exn; - -end; - - -fun init () = edit_history 1 (K (K (Toplevel.toplevel, []))); - -fun goal () = Proof.goal (Toplevel.proof_of (state ())) - handle Toplevel.UNDEF => error "No goal present"; - -fun print () = Toplevel.print_state (state ()); - - -(* history navigation *) - -local - -fun find_and_undo _ [] = error "Undo history exhausted" - | find_and_undo which ((prev, tr) :: hist) = - if which (Toplevel.name_of tr) then (prev, hist) else find_and_undo which hist; - -in - -fun linear_undo n = edit_history n (K (find_and_undo (K true))); - -fun undo n = edit_history n (fn st => fn hist => - find_and_undo (if Toplevel.is_proof st then K true else Keyword.is_theory) hist); - -fun kill () = edit_history 1 (fn st => fn hist => - find_and_undo - (if Toplevel.is_proof st then Keyword.is_theory else Keyword.is_theory_begin) hist); - -fun kill_proof () = edit_history 1 (fn st => fn hist => - if Toplevel.is_proof st then find_and_undo Keyword.is_theory hist - else raise Toplevel.UNDEF); - -end; - - -(* interactive state transformations *) - -fun op >> tr = - (case Toplevel.transition true tr (state ()) of - NONE => false - | SOME (_, SOME exn_info) => - (set_exn (SOME exn_info); - Toplevel.setmp_thread_position tr - Runtime.exn_error_message (Runtime.EXCURSION_FAIL exn_info); - true) - | SOME (st', NONE) => - let - val name = Toplevel.name_of tr; - val _ = if Keyword.is_theory_begin name then init () else (); - val _ = - if Keyword.is_regular name - then edit_history 1 (fn st => fn hist => (st', (st, tr) :: hist)) else (); - in true end); - -fun op >>> [] = () - | op >>> (tr :: trs) = if op >> tr then op >>> trs else (); - - -(* toplevel loop -- uninterruptible *) - -val crashes = Synchronized.var "Isar.crashes" ([]: exn list); - -local - -fun protocol_message props output = - (case props of - function :: args => - if function = Markup.command_timing then - let - val name = the_default "" (Properties.get args Markup.nameN); - val pos = Position.of_properties args; - val timing = Markup.parse_timing_properties args; - in - if Timing.is_relevant timing andalso (! Toplevel.profiling > 0 orelse ! Toplevel.timing) - andalso name <> "" andalso not (Keyword.is_control name) - then tracing ("command " ^ quote name ^ Position.here pos ^ ": " ^ Timing.message timing) - else () - end - else raise Output.Protocol_Message props - | [] => raise Output.Protocol_Message props); - -fun raw_loop secure src = - let - fun check_secure () = - (if secure then warning "Secure loop -- cannot exit to ML" else (); secure); - in - (case Source.get_single (Source.set_prompt Source.default_prompt src) of - NONE => if secure then quit () else () - | SOME (tr, src') => if op >> tr orelse check_secure () then raw_loop secure src' else ()) - handle exn => - (Runtime.exn_error_message exn - handle crash => - (Synchronized.change crashes (cons crash); - warning "Recovering from Isar toplevel crash -- see also Isar.crashes"); - raw_loop secure src) - end; - -in - -fun toplevel_loop in_stream {init = do_init, welcome, sync, secure} = - (Context.set_thread_data NONE; - Multithreading.max_threads_update (Options.default_int "threads"); - if do_init then init () else (); - Output.protocol_message_fn := protocol_message; - if welcome then writeln (Session.welcome ()) else (); - uninterruptible (fn _ => fn () => raw_loop secure (Outer_Syntax.isar in_stream sync)) ()); - -end; - -fun loop () = - toplevel_loop TextIO.stdIn - {init = false, welcome = false, sync = false, secure = Secure.is_secure ()}; - -fun main () = - toplevel_loop TextIO.stdIn - {init = true, welcome = true, sync = false, secure = Secure.is_secure ()}; - -end; diff -r e16712bb1d41 -r cc1e03929685 src/Pure/System/message_channel.ML --- a/src/Pure/System/message_channel.ML Fri Oct 31 17:01:54 2014 +0000 +++ b/src/Pure/System/message_channel.ML Fri Oct 31 23:51:54 2014 +0100 @@ -51,8 +51,7 @@ [] => (flush channel; continue NONE) | msgs => received timeout msgs) and received _ (NONE :: _) = flush channel - | received timeout (SOME msg :: rest) = - (output_message channel msg; received flush_timeout rest) + | received _ (SOME msg :: rest) = (output_message channel msg; received flush_timeout rest) | received timeout [] = continue timeout; in fn () => continue NONE end; diff -r e16712bb1d41 -r cc1e03929685 src/Pure/Thy/thy_info.ML --- a/src/Pure/Thy/thy_info.ML Fri Oct 31 17:01:54 2014 +0000 +++ b/src/Pure/Thy/thy_info.ML Fri Oct 31 23:51:54 2014 +0100 @@ -14,7 +14,6 @@ val get_theory: string -> theory val is_finished: string -> bool val master_directory: string -> Path.T - val loaded_files: string -> Path.T list val remove_thy: string -> unit val kill_thy: string -> unit val use_theories: @@ -22,8 +21,7 @@ (string * Position.T) list -> unit val use_thys: (string * Position.T) list -> unit val use_thy: string * Position.T -> unit - val script_thy: Position.T -> string -> theory - val toplevel_begin_theory: Path.T -> Thy_Header.header -> theory + val script_thy: Position.T -> string -> theory -> theory val register_thy: theory -> unit val finish: unit -> unit end; @@ -126,12 +124,6 @@ val get_imports = Resources.imports_of o get_theory; -(*Proof General legacy*) -fun loaded_files name = NAMED_CRITICAL "Thy_Info" (fn () => - (case get_deps name of - NONE => [] - | SOME {master = (thy_path, _), ...} => thy_path :: Resources.loaded_files (get_theory name))); - (** thy operations **) @@ -143,7 +135,7 @@ else let val succs = thy_graph String_Graph.all_succs [name]; - val _ = Output.urgent_message ("Theory loader: removing " ^ commas_quote succs); + val _ = writeln ("Theory loader: removing " ^ commas_quote succs); val _ = List.app (perform Remove) succs; val _ = change_thys (fold String_Graph.del_node succs); in () end); @@ -269,7 +261,7 @@ fun load_thy document last_timing initiators update_time deps text (name, pos) keywords parents = let val _ = kill_thy name; - val _ = Output.urgent_message ("Loading theory " ^ quote name ^ required_by " " initiators); + val _ = writeln ("Loading theory " ^ quote name ^ required_by " " initiators); val _ = Output.try_protocol_message (Markup.loading_theory name) []; val {master = (thy_path, _), imports} = deps; @@ -378,22 +370,15 @@ (* toplevel scripting -- without maintaining database *) -fun script_thy pos txt = +fun script_thy pos txt thy = let - val trs = Outer_Syntax.parse (Outer_Syntax.get_syntax ()) pos txt; + val trs = + Outer_Syntax.parse (Outer_Syntax.get_syntax ()) pos txt + |> map (Toplevel.modify_init (K thy)); val end_pos = if null trs then pos else Toplevel.pos_of (List.last trs); val end_state = fold (Toplevel.command_exception true) trs Toplevel.toplevel; in Toplevel.end_theory end_pos end_state end; -fun toplevel_begin_theory master_dir (header: Thy_Header.header) = - let - val {name = (name, _), imports, ...} = header; - val _ = kill_thy name; - val _ = use_theories {document = false, last_timing = K NONE, master_dir = master_dir} imports; - val _ = Thy_Header.define_keywords header; - val parents = map (get_theory o base_name o fst) imports; - in Resources.begin_theory master_dir header parents end; - (* register theory *) @@ -405,7 +390,7 @@ in NAMED_CRITICAL "Thy_Info" (fn () => (kill_thy name; - Output.urgent_message ("Registering theory " ^ quote name); + writeln ("Registering theory " ^ quote name); update_thy (make_deps master imports) theory)) end; diff -r e16712bb1d41 -r cc1e03929685 src/Pure/Tools/build.ML --- a/src/Pure/Tools/build.ML Fri Oct 31 17:01:54 2014 +0000 +++ b/src/Pure/Tools/build.ML Fri Oct 31 23:51:54 2014 +0100 @@ -108,8 +108,7 @@ |> Unsynchronized.setmp Multithreading.trace (Options.int options "threads_trace") |> Multithreading.max_threads_setmp (Options.int options "threads") |> Unsynchronized.setmp Future.ML_statistics true - |> Unsynchronized.setmp Pretty.margin_default (Options.int options "pretty_margin") - |> Unsynchronized.setmp Toplevel.timing (Options.bool options "timing"); + |> Unsynchronized.setmp Pretty.margin_default (Options.int options "pretty_margin"); fun use_theories_condition last_timing (options, thys) = let val condition = space_explode "," (Options.string options "condition") in diff -r e16712bb1d41 -r cc1e03929685 src/Pure/Tools/keywords.scala --- a/src/Pure/Tools/keywords.scala Fri Oct 31 17:01:54 2014 +0000 +++ /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 e16712bb1d41 -r cc1e03929685 src/Pure/Tools/proof_general.ML --- a/src/Pure/Tools/proof_general.ML Fri Oct 31 17:01:54 2014 +0000 +++ /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 e16712bb1d41 -r cc1e03929685 src/Pure/Tools/proof_general_pure.ML --- a/src/Pure/Tools/proof_general_pure.ML Fri Oct 31 17:01:54 2014 +0000 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,227 +0,0 @@ -(* Title: Pure/Tools/proof_general_pure.ML - Author: David Aspinall - Author: Makarius - -Proof General setup within theory Pure. -*) - -(*Proof General legacy*) - -structure ProofGeneral_Pure: sig end = -struct - -(** preferences **) - -(* display *) - -val _ = - ProofGeneral.preference_option ProofGeneral.category_display - NONE - @{system_option show_types} - "show-types" - "Include types in display of Isabelle terms"; - -val _ = - ProofGeneral.preference_option ProofGeneral.category_display - NONE - @{system_option show_sorts} - "show-sorts" - "Include sorts in display of Isabelle types"; - -val _ = - ProofGeneral.preference_option ProofGeneral.category_display - NONE - @{system_option show_consts} - "show-consts" - "Show types of consts in Isabelle goal display"; - -val _ = - ProofGeneral.preference_option ProofGeneral.category_display - NONE - @{system_option names_long} - "long-names" - "Show fully qualified names in Isabelle terms"; - -val _ = - ProofGeneral.preference_option ProofGeneral.category_display - NONE - @{system_option show_brackets} - "show-brackets" - "Show full bracketing in Isabelle terms"; - -val _ = - ProofGeneral.preference_option ProofGeneral.category_display - NONE - @{system_option show_main_goal} - "show-main-goal" - "Show main goal in proof state display"; - -val _ = - ProofGeneral.preference_option ProofGeneral.category_display - NONE - @{system_option eta_contract} - "eta-contract" - "Print terms eta-contracted"; - - -(* advanced display *) - -val _ = - ProofGeneral.preference_option ProofGeneral.category_advanced_display - NONE - @{system_option goals_limit} - "goals-limit" - "Setting for maximum number of subgoals to be printed"; - -val _ = - ProofGeneral.preference ProofGeneral.category_advanced_display - NONE - (Markup.print_int o get_default_print_depth) - (default_print_depth o Markup.parse_int) - ProofGeneral.pgipint - "print-depth" - "Setting for the ML print depth"; - -val _ = - ProofGeneral.preference_option ProofGeneral.category_advanced_display - NONE - @{system_option show_question_marks} - "show-question-marks" - "Show leading question mark of variable name"; - - -(* tracing *) - -val _ = - ProofGeneral.preference_bool ProofGeneral.category_tracing - NONE - Raw_Simplifier.simp_trace_default - "trace-simplifier" - "Trace simplification rules"; - -val _ = - ProofGeneral.preference_int ProofGeneral.category_tracing - NONE - Raw_Simplifier.simp_trace_depth_limit_default - "trace-simplifier-depth" - "Trace simplifier depth limit"; - -val _ = - ProofGeneral.preference_bool ProofGeneral.category_tracing - NONE - Pattern.unify_trace_failure_default - "trace-unification" - "Output error diagnostics during unification"; - -val _ = - ProofGeneral.preference_bool ProofGeneral.category_tracing - NONE - Toplevel.timing - "global-timing" - "Whether to enable timing in Isabelle"; - -val _ = - ProofGeneral.preference_option ProofGeneral.category_tracing - NONE - @{system_option ML_exception_trace} - "debugging" - "Whether to enable exception trace for toplevel command execution"; - -val _ = - ProofGeneral.preference_bool ProofGeneral.category_tracing - NONE - ProofGeneral.thm_deps - "theorem-dependencies" - "Track theorem dependencies within Proof General"; - - -(* proof *) - -val _ = - ProofGeneral.preference_option ProofGeneral.category_proof - (SOME "true") - @{system_option quick_and_dirty} - "quick-and-dirty" - "Take a few short cuts"; - -val _ = - ProofGeneral.preference_option ProofGeneral.category_proof - NONE - @{system_option skip_proofs} - "skip-proofs" - "Skip over proofs"; - -val _ = - ProofGeneral.preference ProofGeneral.category_proof - NONE - (Markup.print_bool o Proofterm.proofs_enabled) - (fn s => Proofterm.proofs := (if Markup.parse_bool s then 2 else 0)) - ProofGeneral.pgipbool - "full-proofs" - "Record full proof objects internally"; - -val _ = - ProofGeneral.preference ProofGeneral.category_proof - NONE - (Markup.print_int o Multithreading.max_threads_value) - (Multithreading.max_threads_update o Markup.parse_int) - ProofGeneral.pgipint - "max-threads" - "Maximum number of threads"; - -val _ = - ProofGeneral.preference ProofGeneral.category_proof - NONE - (fn () => Markup.print_bool (! Goal.parallel_proofs >= 1)) - (fn s => Goal.parallel_proofs := (if Markup.parse_bool s then 1 else 0)) - ProofGeneral.pgipint - "parallel-proofs" - "Check proofs in parallel"; - - - -(** command syntax **) - -val _ = - Outer_Syntax.improper_command - @{command_spec "ProofGeneral.process_pgip"} "(internal)" - (Parse.text >> (fn str => Toplevel.imperative (fn () => ProofGeneral.process_pgip str))); - -val _ = - Outer_Syntax.improper_command - @{command_spec "ProofGeneral.pr"} "(internal)" - (Scan.succeed (Toplevel.keep (fn state => - if Toplevel.is_toplevel state orelse Toplevel.is_theory state - then ProofGeneral.tell_clear_goals () - else (Toplevel.quiet := false; Toplevel.print_state state)))); - -val _ = (*undo without output -- historical*) - Outer_Syntax.improper_command - @{command_spec "ProofGeneral.undo"} "(internal)" - (Scan.succeed (Toplevel.imperative (fn () => Isar.undo 1))); - -val _ = - Outer_Syntax.improper_command - @{command_spec "ProofGeneral.restart"} "(internal)" - (Parse.opt_unit >> (K (Toplevel.imperative ProofGeneral.restart))); - -val _ = - Outer_Syntax.improper_command - @{command_spec "ProofGeneral.kill_proof"} "(internal)" - (Scan.succeed (Toplevel.imperative (fn () => - (Isar.kill_proof (); ProofGeneral.tell_clear_goals ())))); - -val _ = - Outer_Syntax.improper_command - @{command_spec "ProofGeneral.inform_file_processed"} "(internal)" - (Parse.name >> (fn file => Toplevel.imperative (fn () => - ProofGeneral.inform_file_processed file))); - -val _ = - Outer_Syntax.improper_command - @{command_spec "ProofGeneral.inform_file_retracted"} "(internal)" - (Parse.name >> (fn file => Toplevel.imperative (fn () => - ProofGeneral.inform_file_retracted file))); - -end; - diff -r e16712bb1d41 -r cc1e03929685 src/Pure/build-jars --- a/src/Pure/build-jars Fri Oct 31 17:01:54 2014 +0000 +++ b/src/Pure/build-jars Fri Oct 31 23:51:54 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 e16712bb1d41 -r cc1e03929685 src/Pure/pure_syn.ML --- a/src/Pure/pure_syn.ML Fri Oct 31 17:01:54 2014 +0000 +++ b/src/Pure/pure_syn.ML Fri Oct 31 23:51:54 2014 +0100 @@ -10,9 +10,8 @@ val _ = 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))); + (Thy_Header.args >> + (fn _ => Toplevel.init_theory (fn () => error "Missing theory initialization"))); val _ = Outer_Syntax.command diff -r e16712bb1d41 -r cc1e03929685 src/Tools/Code/code_printer.ML --- a/src/Tools/Code/code_printer.ML Fri Oct 31 17:01:54 2014 +0000 +++ b/src/Tools/Code/code_printer.ML Fri Oct 31 23:51:54 2014 +0100 @@ -373,7 +373,7 @@ fun read_mixfix s = let - val sym_any = Scan.one Symbol.is_regular; + val sym_any = Scan.one Symbol.not_eof; val parse = Scan.optional ($$ "!" >> K NOBR) BR -- Scan.repeat ( ($$ "(" -- $$ "_" -- $$ ")" >> K (Arg NOBR)) || ($$ "_" >> K (Arg BR)) diff -r e16712bb1d41 -r cc1e03929685 src/Tools/quickcheck.ML --- a/src/Tools/quickcheck.ML Fri Oct 31 17:01:54 2014 +0000 +++ b/src/Tools/quickcheck.ML Fri Oct 31 23:51:54 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 @@ -304,11 +294,11 @@ if is_interactive then exc () else raise TimeLimit.TimeOut else f (); -fun message ctxt s = if Config.get ctxt quiet then () else Output.urgent_message s; +fun message ctxt s = if Config.get ctxt quiet then () else writeln s; fun verbose_message ctxt s = if not (Config.get ctxt quiet) andalso Config.get ctxt verbose - then Output.urgent_message s else (); + then writeln s else (); fun test_terms ctxt (limit_time, is_interactive) insts goals = (case active_testers ctxt of @@ -527,7 +517,7 @@ gen_quickcheck args i (Toplevel.proof_of state) |> apfst (Option.map (the o get_first response_of)) |> (fn (r, state) => - Output.urgent_message (Pretty.string_of + writeln (Pretty.string_of (pretty_counterex (Proof.context_of state) false r))); val parse_arg = @@ -573,7 +563,7 @@ |> (if auto then Proof.goal_message (K (Pretty.mark Markup.information msg)) else - tap (fn _ => Output.urgent_message (Pretty.string_of msg)))) + tap (fn _ => writeln (Pretty.string_of msg)))) else (noneN, state) end) diff -r e16712bb1d41 -r cc1e03929685 src/Tools/solve_direct.ML --- a/src/Tools/solve_direct.ML Fri Oct 31 17:01:54 2014 +0000 +++ b/src/Tools/solve_direct.ML Fri Oct 31 23:51:54 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 *) @@ -90,13 +83,13 @@ Pretty.markup Markup.information (message results)) else tap (fn _ => - Output.urgent_message (Pretty.string_of (Pretty.chunks (message results)))))) + writeln (Pretty.string_of (Pretty.chunks (message results)))))) | SOME NONE => - (if mode = Normal then Output.urgent_message "No proof found." + (if mode = Normal then writeln "No proof found." else (); (noneN, state)) | NONE => - (if mode = Normal then Output.urgent_message "An error occurred." + (if mode = Normal then writeln "An error occurred." else (); (unknownN, state))) end diff -r e16712bb1d41 -r cc1e03929685 src/Tools/try.ML --- a/src/Tools/try.ML Fri Oct 31 17:01:54 2014 +0000 +++ b/src/Tools/try.ML Fri Oct 31 23:51:54 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 _ [] = ["??"] @@ -70,19 +60,19 @@ fun try_tools state = if subgoal_count state = 0 then - (Output.urgent_message "No subgoal!"; NONE) + (writeln "No subgoal!"; NONE) else get_tools (Proof.theory_of state) |> tap (fn tools => "Trying " ^ space_implode " " (serial_commas "and" (map (quote o fst) tools)) ^ "..." - |> Output.urgent_message) + |> writeln) |> Par_List.get_some (fn (name, (_, _, tool)) => case try (tool false) state of SOME (true, (outcome_code, _)) => SOME (name, outcome_code) | _ => NONE) - |> tap (fn NONE => Output.urgent_message "Tried in vain." | _ => ()) + |> tap (fn NONE => writeln "Tried in vain." | _ => ()) val _ = Outer_Syntax.improper_command @{command_spec "try"} @@ -101,17 +91,6 @@ | _ => NONE) |> the_default state -val _ = Context.>> (Specification.add_theorem_hook (fn interact => fn state => - let - val auto_time_limit = Options.default_real @{system_option auto_time_limit} - in - if interact andalso not (!Toplevel.quiet) andalso auto_time_limit > 0.0 then - TimeLimit.timeLimit (seconds auto_time_limit) auto_try state - handle TimeLimit.TimeOut => state - else - state - end)) - (* asynchronous print function (PIDE) *)