merged
authorbulwahn
Mon Mar 21 08:29:16 2011 +0100 (2011-03-21)
changeset 42032143f37194911
parent 42031 2de57cda5b24
parent 42018 878f33040280
child 42033 60350051ef93
merged
src/HOL/Mutabelle/mutabelle_extra.ML
src/HOL/Tools/Predicate_Compile/predicate_compile_quickcheck.ML
src/Tools/quickcheck.ML
     1.1 --- a/NEWS	Fri Mar 18 18:19:42 2011 +0100
     1.2 +++ b/NEWS	Mon Mar 21 08:29:16 2011 +0100
     1.3 @@ -50,6 +50,9 @@
     1.4    - sledgehammer available_provers ~> sledgehammer supported_provers
     1.5      INCOMPATIBILITY.
     1.6  
     1.7 +* "try":
     1.8 +  - Added "simp:", "intro:", and "elim:" options.
     1.9 +
    1.10  * Function package: discontinued option "tailrec".
    1.11  INCOMPATIBILITY. Use partial_function instead.
    1.12  
    1.13 @@ -62,6 +65,9 @@
    1.14  
    1.15  *** ML ***
    1.16  
    1.17 +* Structure Timing provides various operations for timing; supersedes
    1.18 +former start_timing/end_timing etc.
    1.19 +
    1.20  * Path.print is the official way to show file-system paths to users
    1.21  (including quotes etc.).
    1.22  
     2.1 --- a/doc-src/System/Thy/Presentation.thy	Fri Mar 18 18:19:42 2011 +0100
     2.2 +++ b/doc-src/System/Thy/Presentation.thy	Mon Mar 21 08:29:16 2011 +0100
     2.3 @@ -448,7 +448,7 @@
     2.4      -P PATH      set path for remote theory browsing information
     2.5      -Q INT       set threshold for sub-proof parallelization (default 50)
     2.6      -T LEVEL     multithreading: trace level (default 0)
     2.7 -    -V VERSION   declare alternative document VERSION
     2.8 +    -V VARIANT   declare alternative document VARIANT
     2.9      -b           build mode (output heap image, using current dir)
    2.10      -d FORMAT    build document as FORMAT (default false)
    2.11      -f NAME      use ML file NAME (default ROOT.ML)
    2.12 @@ -523,16 +523,16 @@
    2.13    \secref{sec:tool-latex} for more details.
    2.14  
    2.15    \medskip The @{verbatim "-V"} option declares alternative document
    2.16 -  versions, consisting of name/tags pairs (cf.\ options @{verbatim
    2.17 +  variants, consisting of name/tags pairs (cf.\ options @{verbatim
    2.18    "-n"} and @{verbatim "-t"} of the @{tool_ref document} tool).  The
    2.19    standard document is equivalent to ``@{verbatim
    2.20    "document=theory,proof,ML"}'', which means that all theory begin/end
    2.21    commands, proof body texts, and ML code will be presented
    2.22 -  faithfully.  An alternative version ``@{verbatim
    2.23 +  faithfully.  An alternative variant ``@{verbatim
    2.24    "outline=/proof/ML"}'' would fold proof and ML parts, replacing the
    2.25    original text by a short place-holder.  The form ``@{text
    2.26    name}@{verbatim "=-"},'' means to remove document @{text name} from
    2.27 -  the list of versions to be processed.  Any number of @{verbatim
    2.28 +  the list of variants to be processed.  Any number of @{verbatim
    2.29    "-V"} options may be given; later declarations have precedence over
    2.30    earlier ones.
    2.31  
    2.32 @@ -682,15 +682,15 @@
    2.33    corresponding output files named after @{verbatim root} as well,
    2.34    e.g.\ @{verbatim root.dvi} for target format @{verbatim dvi}.
    2.35  
    2.36 -  \medskip When running the session, Isabelle copies the original
    2.37 -  @{verbatim document} directory into its proper place within
    2.38 -  @{setting ISABELLE_BROWSER_INFO} according to the session path.
    2.39 -  Then, for any processed theory @{text A} some {\LaTeX} source is
    2.40 -  generated and put there as @{text A}@{verbatim ".tex"}.
    2.41 -  Furthermore, a list of all generated theory files is put into
    2.42 -  @{verbatim session.tex}.  Typically, the root {\LaTeX} file provided
    2.43 -  by the user would include @{verbatim session.tex} to get a document
    2.44 -  containing all the theories.
    2.45 +  \medskip When running the session, Isabelle copies the content of
    2.46 +  the original @{verbatim document} directory into its proper place
    2.47 +  within @{setting ISABELLE_BROWSER_INFO}, according to the session
    2.48 +  path and document variant.  Then, for any processed theory @{text A}
    2.49 +  some {\LaTeX} source is generated and put there as @{text
    2.50 +  A}@{verbatim ".tex"}.  Furthermore, a list of all generated theory
    2.51 +  files is put into @{verbatim session.tex}.  Typically, the root
    2.52 +  {\LaTeX} file provided by the user would include @{verbatim
    2.53 +  session.tex} to get a document containing all the theories.
    2.54  
    2.55    The {\LaTeX} versions of the theories require some macros defined in
    2.56    @{file "~~/lib/texinputs/isabelle.sty"}.  Doing @{verbatim
     3.1 --- a/doc-src/System/Thy/document/Presentation.tex	Fri Mar 18 18:19:42 2011 +0100
     3.2 +++ b/doc-src/System/Thy/document/Presentation.tex	Mon Mar 21 08:29:16 2011 +0100
     3.3 @@ -474,7 +474,7 @@
     3.4      -P PATH      set path for remote theory browsing information
     3.5      -Q INT       set threshold for sub-proof parallelization (default 50)
     3.6      -T LEVEL     multithreading: trace level (default 0)
     3.7 -    -V VERSION   declare alternative document VERSION
     3.8 +    -V VARIANT   declare alternative document VARIANT
     3.9      -b           build mode (output heap image, using current dir)
    3.10      -d FORMAT    build document as FORMAT (default false)
    3.11      -f NAME      use ML file NAME (default ROOT.ML)
    3.12 @@ -550,12 +550,12 @@
    3.13    \secref{sec:tool-latex} for more details.
    3.14  
    3.15    \medskip The \verb|-V| option declares alternative document
    3.16 -  versions, consisting of name/tags pairs (cf.\ options \verb|-n| and \verb|-t| of the \indexref{}{tool}{document}\hyperlink{tool.document}{\mbox{\isa{\isatt{document}}}} tool).  The
    3.17 +  variants, consisting of name/tags pairs (cf.\ options \verb|-n| and \verb|-t| of the \indexref{}{tool}{document}\hyperlink{tool.document}{\mbox{\isa{\isatt{document}}}} tool).  The
    3.18    standard document is equivalent to ``\verb|document=theory,proof,ML|'', which means that all theory begin/end
    3.19    commands, proof body texts, and ML code will be presented
    3.20 -  faithfully.  An alternative version ``\verb|outline=/proof/ML|'' would fold proof and ML parts, replacing the
    3.21 +  faithfully.  An alternative variant ``\verb|outline=/proof/ML|'' would fold proof and ML parts, replacing the
    3.22    original text by a short place-holder.  The form ``\isa{name}\verb|=-|,'' means to remove document \isa{name} from
    3.23 -  the list of versions to be processed.  Any number of \verb|-V| options may be given; later declarations have precedence over
    3.24 +  the list of variants to be processed.  Any number of \verb|-V| options may be given; later declarations have precedence over
    3.25    earlier ones.
    3.26  
    3.27    \medskip The \verb|-g| option produces images of the theory
    3.28 @@ -693,15 +693,13 @@
    3.29    corresponding output files named after \verb|root| as well,
    3.30    e.g.\ \verb|root.dvi| for target format \verb|dvi|.
    3.31  
    3.32 -  \medskip When running the session, Isabelle copies the original
    3.33 -  \verb|document| directory into its proper place within
    3.34 -  \hyperlink{setting.ISABELLE-BROWSER-INFO}{\mbox{\isa{\isatt{ISABELLE{\isaliteral{5F}{\isacharunderscore}}BROWSER{\isaliteral{5F}{\isacharunderscore}}INFO}}}} according to the session path.
    3.35 -  Then, for any processed theory \isa{A} some {\LaTeX} source is
    3.36 -  generated and put there as \isa{A}\verb|.tex|.
    3.37 -  Furthermore, a list of all generated theory files is put into
    3.38 -  \verb|session.tex|.  Typically, the root {\LaTeX} file provided
    3.39 -  by the user would include \verb|session.tex| to get a document
    3.40 -  containing all the theories.
    3.41 +  \medskip When running the session, Isabelle copies the content of
    3.42 +  the original \verb|document| directory into its proper place
    3.43 +  within \hyperlink{setting.ISABELLE-BROWSER-INFO}{\mbox{\isa{\isatt{ISABELLE{\isaliteral{5F}{\isacharunderscore}}BROWSER{\isaliteral{5F}{\isacharunderscore}}INFO}}}}, according to the session
    3.44 +  path and document variant.  Then, for any processed theory \isa{A}
    3.45 +  some {\LaTeX} source is generated and put there as \isa{A}\verb|.tex|.  Furthermore, a list of all generated theory
    3.46 +  files is put into \verb|session.tex|.  Typically, the root
    3.47 +  {\LaTeX} file provided by the user would include \verb|session.tex| to get a document containing all the theories.
    3.48  
    3.49    The {\LaTeX} versions of the theories require some macros defined in
    3.50    \verb|~~/lib/texinputs/isabelle.sty|.  Doing \verb|\usepackage{isabelle}| in \verb|root.tex| should be fine;
     4.1 --- a/lib/Tools/usedir	Fri Mar 18 18:19:42 2011 +0100
     4.2 +++ b/lib/Tools/usedir	Mon Mar 21 08:29:16 2011 +0100
     4.3 @@ -21,7 +21,7 @@
     4.4    echo "    -P PATH      set path for remote theory browsing information"
     4.5    echo "    -Q INT       set threshold for sub-proof parallelization (default 100)"
     4.6    echo "    -T LEVEL     multithreading: trace level (default 0)"
     4.7 -  echo "    -V VERSION   declare alternative document VERSION"
     4.8 +  echo "    -V VARIANT   declare alternative document VARIANT"
     4.9    echo "    -b           build mode (output heap image, using current dir)"
    4.10    echo "    -d FORMAT    build document as FORMAT (default false)"
    4.11    echo "    -f NAME      use ML file NAME (default ROOT.ML)"
    4.12 @@ -74,7 +74,7 @@
    4.13  MAXTHREADS="1"
    4.14  RPATH=""
    4.15  TRACETHREADS="0"
    4.16 -DOCUMENT_VERSIONS=""
    4.17 +DOCUMENT_VARIANTS=""
    4.18  BUILD=""
    4.19  DOCUMENT=false
    4.20  ROOT_FILE="ROOT.ML"
    4.21 @@ -122,10 +122,10 @@
    4.22          TRACETHREADS="$OPTARG"
    4.23          ;;
    4.24        V)
    4.25 -        if [ -z "$DOCUMENT_VERSIONS" ]; then
    4.26 -          DOCUMENT_VERSIONS="\"$OPTARG\""
    4.27 +        if [ -z "$DOCUMENT_VARIANTS" ]; then
    4.28 +          DOCUMENT_VARIANTS="\"$OPTARG\""
    4.29          else
    4.30 -          DOCUMENT_VERSIONS="$DOCUMENT_VERSIONS, \"$OPTARG\""
    4.31 +          DOCUMENT_VARIANTS="$DOCUMENT_VARIANTS, \"$OPTARG\""
    4.32          fi
    4.33          ;;
    4.34        b)
    4.35 @@ -241,7 +241,7 @@
    4.36    LOG="$LOGDIR/$ITEM"
    4.37  
    4.38    "$ISABELLE_PROCESS" \
    4.39 -    -e "Session.use_dir \"$ITEM\" \"$ROOT_FILE\" true [$MODES] $RESET $INFO \"$DOC\" $DOCUMENT_GRAPH [$DOCUMENT_VERSIONS] \"$PARENT\" \"$SESSION\" ($COPY_DUMP, \"$DUMP\") \"$RPATH\" $PROOFS $TIMING $VERBOSE $MAXTHREADS $TRACETHREADS $PARALLEL_PROOFS $PARALLEL_PROOFS_THRESHOLD;" \
    4.40 +    -e "Session.use_dir \"$ITEM\" \"$ROOT_FILE\" true [$MODES] $RESET $INFO \"$DOC\" $DOCUMENT_GRAPH [$DOCUMENT_VARIANTS] \"$PARENT\" \"$SESSION\" ($COPY_DUMP, \"$DUMP\") \"$RPATH\" $PROOFS $TIMING $VERBOSE $MAXTHREADS $TRACETHREADS $PARALLEL_PROOFS $PARALLEL_PROOFS_THRESHOLD;" \
    4.41      -q -w $LOGIC $NAME > "$LOG"
    4.42    RC="$?"
    4.43  else
    4.44 @@ -250,7 +250,7 @@
    4.45    LOG="$LOGDIR/$ITEM"
    4.46  
    4.47    "$ISABELLE_PROCESS" \
    4.48 -    -e "Session.use_dir \"$ITEM\" \"$ROOT_FILE\" false [$MODES] $RESET $INFO \"$DOC\" $DOCUMENT_GRAPH [$DOCUMENT_VERSIONS] \"$PARENT\" \"$SESSION\" ($COPY_DUMP, \"$DUMP\") \"$RPATH\" $PROOFS $TIMING $VERBOSE $MAXTHREADS $TRACETHREADS $PARALLEL_PROOFS $PARALLEL_PROOFS_THRESHOLD; quit();" \
    4.49 +    -e "Session.use_dir \"$ITEM\" \"$ROOT_FILE\" false [$MODES] $RESET $INFO \"$DOC\" $DOCUMENT_GRAPH [$DOCUMENT_VARIANTS] \"$PARENT\" \"$SESSION\" ($COPY_DUMP, \"$DUMP\") \"$RPATH\" $PROOFS $TIMING $VERBOSE $MAXTHREADS $TRACETHREADS $PARALLEL_PROOFS $PARALLEL_PROOFS_THRESHOLD; quit();" \
    4.50      -r -q "$LOGIC" > "$LOG"
    4.51    RC="$?"
    4.52    cd ..
     5.1 --- a/src/HOL/Boogie/Tools/boogie_commands.ML	Fri Mar 18 18:19:42 2011 +0100
     5.2 +++ b/src/HOL/Boogie/Tools/boogie_commands.ML	Mon Mar 21 08:29:16 2011 +0100
     5.3 @@ -22,8 +22,7 @@
     5.4          "expected file ending " ^ quote ext)
     5.5  
     5.6      val base_path = Path.explode base_name |> tap check_ext
     5.7 -    val (full_path, _) =
     5.8 -      Thy_Load.check_file (Thy_Load.master_directory thy) base_path
     5.9 +    val full_path = Thy_Load.check_file (Thy_Load.master_directory thy) base_path
    5.10  
    5.11      val _ = Boogie_VCs.is_closed thy orelse
    5.12        error ("Found the beginning of a new Boogie environment, " ^
     6.1 --- a/src/HOL/Matrix/Compute_Oracle/report.ML	Fri Mar 18 18:19:42 2011 +0100
     6.2 +++ b/src/HOL/Matrix/Compute_Oracle/report.ML	Mon Mar 21 08:29:16 2011 +0100
     6.3 @@ -11,9 +11,9 @@
     6.4  
     6.5  fun timeit f =
     6.6      let
     6.7 -        val t1 = start_timing ()
     6.8 +        val t1 = Timing.start ()
     6.9          val x = f ()
    6.10 -        val t2 = #message (end_timing t1)
    6.11 +        val t2 = Timing.message (Timing.result t1)
    6.12          val _ = writeln ((report_space ()) ^ "--> "^t2)
    6.13      in
    6.14          x       
     7.1 --- a/src/HOL/Mirabelle/Tools/mirabelle.ML	Fri Mar 18 18:19:42 2011 +0100
     7.2 +++ b/src/HOL/Mirabelle/Tools/mirabelle.ML	Mon Mar 21 08:29:16 2011 +0100
     7.3 @@ -210,10 +210,7 @@
     7.4    | NONE => default)
     7.5  
     7.6  fun cpu_time f x =
     7.7 -  let
     7.8 -    val start = start_timing ()
     7.9 -    val result = Exn.capture (fn () => f x) ()
    7.10 -    val time = Time.toMilliseconds (#cpu (end_timing start))
    7.11 -  in (Exn.release result, time) end
    7.12 +  let val ({cpu, ...}, y) = Timing.timing f x
    7.13 +  in (y, Time.toMilliseconds cpu) end
    7.14  
    7.15  end
     8.1 --- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML	Fri Mar 18 18:19:42 2011 +0100
     8.2 +++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML	Mon Mar 21 08:29:16 2011 +0100
     8.3 @@ -558,7 +558,7 @@
     8.4          Unsynchronized.ref (NONE : ((string * locality) * thm list) list option)
     8.5        val minimize = AList.defined (op =) args minimizeK
     8.6        val metis_ft = AList.defined (op =) args metis_ftK
     8.7 -      val trivial = Try.invoke_try (SOME try_timeout) pre
     8.8 +      val trivial = Try.invoke_try (SOME try_timeout) ([], [], []) pre
     8.9          handle TimeLimit.TimeOut => false
    8.10        fun apply_reconstructor m1 m2 =
    8.11          if metis_ft
     9.1 --- a/src/HOL/Mutabelle/mutabelle_extra.ML	Fri Mar 18 18:19:42 2011 +0100
     9.2 +++ b/src/HOL/Mutabelle/mutabelle_extra.ML	Mon Mar 21 08:29:16 2011 +0100
     9.3 @@ -150,7 +150,7 @@
     9.4    let
     9.5      val state = Proof.theorem NONE (K I) (map (single o rpair []) [t]) (ProofContext.init_global thy)
     9.6    in
     9.7 -    case Try.invoke_try (SOME (seconds 5.0)) state of
     9.8 +    case Try.invoke_try (SOME (seconds 5.0)) ([], [], []) state of
     9.9        true => (Solved, ([], NONE))
    9.10      | false => (Unsolved, ([], NONE))
    9.11    end
    9.12 @@ -332,12 +332,9 @@
    9.13  
    9.14  fun count x = (length oo filter o equal) x
    9.15  
    9.16 -fun cpu_time description f =
    9.17 -  let
    9.18 -    val start = start_timing ()
    9.19 -    val result = Exn.capture f ()
    9.20 -    val time = Time.toMilliseconds (#cpu (end_timing start))
    9.21 -  in (Exn.release result, (description, time)) end
    9.22 +fun cpu_time description e =
    9.23 +  let val ({cpu, ...}, result) = Timing.timing e ()
    9.24 +  in (result, (description, Time.toMilliseconds cpu)) end
    9.25  (*
    9.26  fun unsafe_invoke_mtd thy (mtd_name, invoke_mtd) t =
    9.27    let
    10.1 --- a/src/HOL/SPARK/Tools/spark_commands.ML	Fri Mar 18 18:19:42 2011 +0100
    10.2 +++ b/src/HOL/SPARK/Tools/spark_commands.ML	Mon Mar 21 08:29:16 2011 +0100
    10.3 @@ -15,8 +15,7 @@
    10.4  
    10.5  fun spark_open vc_name thy =
    10.6    let
    10.7 -    val (vc_path, _) = Thy_Load.check_file
    10.8 -      (Thy_Load.master_directory thy) (Path.explode vc_name);
    10.9 +    val vc_path = Thy_Load.check_file (Thy_Load.master_directory thy) (Path.explode vc_name);
   10.10      val (base, header) =
   10.11        (case Path.split_ext vc_path of
   10.12          (base, "vcg") => (base, Fdl_Lexer.vcg_header >> K ())
    11.1 --- a/src/HOL/TLA/Action.thy	Fri Mar 18 18:19:42 2011 +0100
    11.2 +++ b/src/HOL/TLA/Action.thy	Mon Mar 21 08:29:16 2011 +0100
    11.3 @@ -12,9 +12,8 @@
    11.4  
    11.5  (** abstract syntax **)
    11.6  
    11.7 -types
    11.8 -  'a trfun = "(state * state) => 'a"
    11.9 -  action   = "bool trfun"
   11.10 +type_synonym 'a trfun = "(state * state) => 'a"
   11.11 +type_synonym action   = "bool trfun"
   11.12  
   11.13  arities prod :: (world, world) world
   11.14  
    12.1 --- a/src/HOL/TLA/Init.thy	Fri Mar 18 18:19:42 2011 +0100
    12.2 +++ b/src/HOL/TLA/Init.thy	Mon Mar 21 08:29:16 2011 +0100
    12.3 @@ -14,8 +14,7 @@
    12.4  typedecl behavior
    12.5  arities behavior :: world
    12.6  
    12.7 -types
    12.8 -  temporal = "behavior form"
    12.9 +type_synonym temporal = "behavior form"
   12.10  
   12.11  
   12.12  consts
    13.1 --- a/src/HOL/TLA/Intensional.thy	Fri Mar 18 18:19:42 2011 +0100
    13.2 +++ b/src/HOL/TLA/Intensional.thy	Mon Mar 21 08:29:16 2011 +0100
    13.3 @@ -15,9 +15,8 @@
    13.4  
    13.5  (** abstract syntax **)
    13.6  
    13.7 -types
    13.8 -  ('w,'a) expr = "'w => 'a"               (* intention: 'w::world, 'a::type *)
    13.9 -  'w form = "('w, bool) expr"
   13.10 +type_synonym ('w,'a) expr = "'w => 'a"   (* intention: 'w::world, 'a::type *)
   13.11 +type_synonym 'w form = "('w, bool) expr"
   13.12  
   13.13  consts
   13.14    Valid    :: "('w::world) form => bool"
    14.1 --- a/src/HOL/TLA/Memory/MemClerk.thy	Fri Mar 18 18:19:42 2011 +0100
    14.2 +++ b/src/HOL/TLA/Memory/MemClerk.thy	Mon Mar 21 08:29:16 2011 +0100
    14.3 @@ -8,11 +8,10 @@
    14.4  imports Memory RPC MemClerkParameters
    14.5  begin
    14.6  
    14.7 -types
    14.8 -  (* The clerk takes the same arguments as the memory and sends requests to the RPC *)
    14.9 -  mClkSndChType = "memChType"
   14.10 -  mClkRcvChType = "rpcSndChType"
   14.11 -  mClkStType    = "(PrIds => mClkState) stfun"
   14.12 +(* The clerk takes the same arguments as the memory and sends requests to the RPC *)
   14.13 +type_synonym mClkSndChType = "memChType"
   14.14 +type_synonym mClkRcvChType = "rpcSndChType"
   14.15 +type_synonym mClkStType = "(PrIds => mClkState) stfun"
   14.16  
   14.17  definition
   14.18    (* state predicates *)
    15.1 --- a/src/HOL/TLA/Memory/MemClerkParameters.thy	Fri Mar 18 18:19:42 2011 +0100
    15.2 +++ b/src/HOL/TLA/Memory/MemClerkParameters.thy	Mon Mar 21 08:29:16 2011 +0100
    15.3 @@ -10,11 +10,10 @@
    15.4  
    15.5  datatype mClkState = clkA | clkB
    15.6  
    15.7 -types
    15.8 -  (* types sent on the clerk's send and receive channels are argument types
    15.9 -     of the memory and the RPC, respectively *)
   15.10 -  mClkSndArgType   = "memOp"
   15.11 -  mClkRcvArgType   = "rpcOp"
   15.12 +(* types sent on the clerk's send and receive channels are argument types
   15.13 +   of the memory and the RPC, respectively *)
   15.14 +type_synonym mClkSndArgType = "memOp"
   15.15 +type_synonym mClkRcvArgType = "rpcOp"
   15.16  
   15.17  definition
   15.18    (* translate a memory call to an RPC call *)
    16.1 --- a/src/HOL/TLA/Memory/Memory.thy	Fri Mar 18 18:19:42 2011 +0100
    16.2 +++ b/src/HOL/TLA/Memory/Memory.thy	Mon Mar 21 08:29:16 2011 +0100
    16.3 @@ -8,10 +8,9 @@
    16.4  imports MemoryParameters ProcedureInterface
    16.5  begin
    16.6  
    16.7 -types
    16.8 -  memChType  = "(memOp, Vals) channel"
    16.9 -  memType = "(Locs => Vals) stfun"      (* intention: MemLocs => MemVals *)
   16.10 -  resType = "(PrIds => Vals) stfun"
   16.11 +type_synonym memChType = "(memOp, Vals) channel"
   16.12 +type_synonym memType = "(Locs => Vals) stfun"  (* intention: MemLocs => MemVals *)
   16.13 +type_synonym resType = "(PrIds => Vals) stfun"
   16.14  
   16.15  consts
   16.16    (* state predicates *)
    17.1 --- a/src/HOL/TLA/Memory/MemoryImplementation.thy	Fri Mar 18 18:19:42 2011 +0100
    17.2 +++ b/src/HOL/TLA/Memory/MemoryImplementation.thy	Mon Mar 21 08:29:16 2011 +0100
    17.3 @@ -10,8 +10,7 @@
    17.4  
    17.5  datatype histState = histA | histB
    17.6  
    17.7 -types
    17.8 -  histType  = "(PrIds => histState) stfun"     (* the type of the history variable *)
    17.9 +type_synonym histType = "(PrIds => histState) stfun"  (* the type of the history variable *)
   17.10  
   17.11  consts
   17.12    (* the specification *)
    18.1 --- a/src/HOL/TLA/Memory/ProcedureInterface.thy	Fri Mar 18 18:19:42 2011 +0100
    18.2 +++ b/src/HOL/TLA/Memory/ProcedureInterface.thy	Mon Mar 21 08:29:16 2011 +0100
    18.3 @@ -8,15 +8,13 @@
    18.4  imports "../TLA" RPCMemoryParams
    18.5  begin
    18.6  
    18.7 -typedecl
    18.8 +typedecl ('a,'r) chan
    18.9    (* type of channels with argument type 'a and return type 'r.
   18.10       we model a channel as an array of variables (of type chan)
   18.11       rather than a single array-valued variable because the
   18.12       notation gets a little simpler.
   18.13    *)
   18.14 -  ('a,'r) chan
   18.15 -types
   18.16 -  ('a,'r) channel =" (PrIds => ('a,'r) chan) stfun"
   18.17 +type_synonym ('a,'r) channel =" (PrIds => ('a,'r) chan) stfun"
   18.18  
   18.19  consts
   18.20    (* data-level functions *)
    19.1 --- a/src/HOL/TLA/Memory/RPC.thy	Fri Mar 18 18:19:42 2011 +0100
    19.2 +++ b/src/HOL/TLA/Memory/RPC.thy	Mon Mar 21 08:29:16 2011 +0100
    19.3 @@ -8,10 +8,9 @@
    19.4  imports RPCParameters ProcedureInterface Memory
    19.5  begin
    19.6  
    19.7 -types
    19.8 -  rpcSndChType  = "(rpcOp,Vals) channel"
    19.9 -  rpcRcvChType  = "memChType"
   19.10 -  rpcStType     = "(PrIds => rpcState) stfun"
   19.11 +type_synonym rpcSndChType = "(rpcOp,Vals) channel"
   19.12 +type_synonym rpcRcvChType = "memChType"
   19.13 +type_synonym rpcStType = "(PrIds => rpcState) stfun"
   19.14  
   19.15  consts
   19.16    (* state predicates *)
    20.1 --- a/src/HOL/TLA/Memory/RPCMemoryParams.thy	Fri Mar 18 18:19:42 2011 +0100
    20.2 +++ b/src/HOL/TLA/Memory/RPCMemoryParams.thy	Mon Mar 21 08:29:16 2011 +0100
    20.3 @@ -8,10 +8,10 @@
    20.4  imports Main
    20.5  begin
    20.6  
    20.7 -types
    20.8 -  bit = "bool"   (* Signal wires for the procedure interface.
    20.9 -                    Defined as bool for simplicity. All I should really need is
   20.10 -                    the existence of two distinct values. *)
   20.11 +type_synonym bit = "bool"
   20.12 + (* Signal wires for the procedure interface.
   20.13 +    Defined as bool for simplicity. All I should really need is
   20.14 +    the existence of two distinct values. *)
   20.15  
   20.16  (* all of these are simple (HOL) types *)
   20.17  typedecl Locs    (* "syntactic" value type *)
    21.1 --- a/src/HOL/TLA/Stfun.thy	Fri Mar 18 18:19:42 2011 +0100
    21.2 +++ b/src/HOL/TLA/Stfun.thy	Mon Mar 21 08:29:16 2011 +0100
    21.3 @@ -13,9 +13,8 @@
    21.4  
    21.5  arities state :: world
    21.6  
    21.7 -types
    21.8 -  'a stfun = "state => 'a"
    21.9 -  stpred  = "bool stfun"
   21.10 +type_synonym 'a stfun = "state => 'a"
   21.11 +type_synonym stpred  = "bool stfun"
   21.12  
   21.13  
   21.14  consts
    22.1 --- a/src/HOL/Tools/Nitpick/nitpick_kodkod.ML	Fri Mar 18 18:19:42 2011 +0100
    22.2 +++ b/src/HOL/Tools/Nitpick/nitpick_kodkod.ML	Mon Mar 21 08:29:16 2011 +0100
    22.3 @@ -300,6 +300,24 @@
    22.4    | bound_for_plain_rel _ _ u =
    22.5      raise NUT ("Nitpick_Kodkod.bound_for_plain_rel", [u])
    22.6  
    22.7 +fun is_datatype_nat_like ({typ, constrs, ...} : datatype_spec) =
    22.8 +  case constrs of
    22.9 +    [_, _] =>
   22.10 +    (case constrs |> map (snd o #const) |> List.partition is_fun_type of
   22.11 +       ([Type (_, Ts1)], [T2]) => forall (curry (op =) typ) (T2 :: Ts1)
   22.12 +     | _ => false)
   22.13 +  | _ => false
   22.14 +
   22.15 +fun needed_values need_vals T =
   22.16 +  AList.lookup (op =) need_vals T |> the_default NONE |> these
   22.17 +
   22.18 +fun all_values_are_needed need_vals ({typ, card, ...} : datatype_spec) =
   22.19 +  length (needed_values need_vals typ) = card
   22.20 +
   22.21 +fun is_sel_of_constr x (Construct (sel_us, _, _, _), _) =
   22.22 +    exists (fn FreeRel (x', _, _, _) => x = x' | _ => false) sel_us
   22.23 +  | is_sel_of_constr _ _ = false
   22.24 +
   22.25  fun bound_for_sel_rel ctxt debug need_vals dtypes
   22.26          (FreeRel (x, T as Type (@{type_name fun}, [T1, T2]),
   22.27                    R as Func (Atom (_, j0), R2), nick)) =
   22.28 @@ -308,46 +326,80 @@
   22.29        val {delta, epsilon, exclusive, explicit_max, ...} =
   22.30          constr_spec dtypes (constr_s, T1)
   22.31        val dtype as {card, ...} = datatype_spec dtypes T1 |> the
   22.32 -      val need_vals =
   22.33 -        AList.lookup (op =) need_vals T1 |> the_default NONE |> these
   22.34 +      val T1_need_vals = needed_values need_vals T1
   22.35      in
   22.36        ([(x, bound_comment ctxt debug nick T R)],
   22.37         let
   22.38 -         val complete_need_vals = (length need_vals = card)
   22.39 +         val discr = (R2 = Formula Neut)
   22.40 +         val complete_need_vals = (length T1_need_vals = card)
   22.41           val (my_need_vals, other_need_vals) =
   22.42 -           need_vals
   22.43 -           |> List.partition
   22.44 -                  (fn (Construct (sel_us, _, _, _), _) =>
   22.45 -                      exists (fn FreeRel (x', _, _, _) => x = x'
   22.46 -                               | _ => false) sel_us
   22.47 -                    | _ => false)
   22.48 -         fun upper_bound_ts () =
   22.49 -           if complete_need_vals then
   22.50 -             my_need_vals |> map (KK.Tuple o single o snd) |> KK.TupleSet
   22.51 -           else if not (null other_need_vals) then
   22.52 -             index_seq (delta + j0) (epsilon - delta)
   22.53 -             |> filter_out (member (op = o apsnd snd) other_need_vals)
   22.54 -             |> map (KK.Tuple o single) |> KK.TupleSet
   22.55 +           T1_need_vals |> List.partition (is_sel_of_constr x)
   22.56 +         fun atom_seq_for_self_rec j =
   22.57 +           if is_datatype_nat_like dtype then (1, j + j0 - 1) else (j, j0)
   22.58 +         fun exact_bound_for_perhaps_needy_atom j =
   22.59 +           case AList.find (op =) my_need_vals j of
   22.60 +             [constr_u] =>
   22.61 +             let
   22.62 +               val n = sel_no_from_name nick
   22.63 +               val arg_u =
   22.64 +                 case constr_u of
   22.65 +                   Construct (_, _, _, arg_us) => nth arg_us n
   22.66 +                 | _ => raise Fail "expected \"Construct\""
   22.67 +               val T2_need_vals = needed_values need_vals T2
   22.68 +             in
   22.69 +               case AList.lookup (op =) T2_need_vals arg_u of
   22.70 +                 SOME arg_j => SOME (KK.TupleAtomSeq (1, arg_j))
   22.71 +               | _ => NONE
   22.72 +             end
   22.73 +           | _ => NONE
   22.74 +         fun n_fold_tuple_union [] = KK.TupleSet []
   22.75 +           | n_fold_tuple_union (ts :: tss) =
   22.76 +             fold (curry (KK.TupleUnion o swap)) tss ts
   22.77 +         fun tuple_perhaps_needy_atom upper j =
   22.78 +           single_atom j
   22.79 +           |> not discr
   22.80 +              ? (fn ts => KK.TupleProduct (ts,
   22.81 +                              case exact_bound_for_perhaps_needy_atom j of
   22.82 +                                SOME ts => ts
   22.83 +                              | NONE => if upper then upper_bound_for_rep R2
   22.84 +                                        else KK.TupleSet []))
   22.85 +         fun bound_tuples upper =
   22.86 +           if null T1_need_vals then
   22.87 +             if upper then
   22.88 +               KK.TupleAtomSeq (epsilon - delta, delta + j0)
   22.89 +               |> not discr
   22.90 +                  ? (fn ts => KK.TupleProduct (ts, upper_bound_for_rep R2))
   22.91 +             else
   22.92 +               KK.TupleSet []
   22.93             else
   22.94 -             KK.TupleAtomSeq (epsilon - delta, delta + j0)
   22.95 +             (if complete_need_vals then
   22.96 +                my_need_vals |> map snd
   22.97 +              else
   22.98 +                index_seq (delta + j0) (epsilon - delta)
   22.99 +                |> filter_out (member (op = o apsnd snd) other_need_vals))
  22.100 +             |> map (tuple_perhaps_needy_atom upper)
  22.101 +             |> n_fold_tuple_union
  22.102         in
  22.103           if explicit_max = 0 orelse
  22.104 -            (complete_need_vals andalso null my_need_vals) (* ### needed? *) then
  22.105 +            (complete_need_vals andalso null my_need_vals) then
  22.106             [KK.TupleSet []]
  22.107           else
  22.108 -           if R2 = Formula Neut then
  22.109 -             [upper_bound_ts ()] |> not exclusive ? cons (KK.TupleSet [])
  22.110 +           if discr then
  22.111 +             [bound_tuples true]
  22.112 +             |> not (exclusive orelse all_values_are_needed need_vals dtype)
  22.113 +                ? cons (KK.TupleSet [])
  22.114             else
  22.115 -             [KK.TupleSet [],
  22.116 +             [bound_tuples false,
  22.117                if T1 = T2 andalso epsilon > delta andalso
  22.118                   is_datatype_acyclic dtype then
  22.119                  index_seq delta (epsilon - delta)
  22.120                  |> map (fn j =>
  22.121                             KK.TupleProduct (KK.TupleSet [KK.Tuple [j + j0]],
  22.122 -                                            KK.TupleAtomSeq (j, j0)))
  22.123 -                |> foldl1 KK.TupleUnion
  22.124 +                               KK.TupleAtomSeq (atom_seq_for_self_rec j)))
  22.125 +                |> n_fold_tuple_union
  22.126                else
  22.127 -                KK.TupleProduct (upper_bound_ts (), upper_bound_for_rep R2)]
  22.128 +                bound_tuples true]
  22.129 +             |> distinct (op =)
  22.130           end)
  22.131      end
  22.132    | bound_for_sel_rel _ _ _ _ u =
  22.133 @@ -1499,14 +1551,14 @@
  22.134    let val dummy_u = RelReg (0, type_of u, rep_of u) in
  22.135      case Op2 (DefEq, bool_T, Formula Pos, dummy_u, u)
  22.136           |> kodkod_formula_from_nut ofs kk of
  22.137 -      KK.RelEq (KK.RelReg _, r) => KK.RelEq (KK.Atom j, r)
  22.138 +      KK.RelEq (KK.RelReg _, r) => SOME (KK.RelEq (KK.Atom j, r))
  22.139      | _ => raise BAD ("Nitpick_Kodkod.atom_equation_for_nut",
  22.140                        "malformed Kodkod formula")
  22.141    end
  22.142  
  22.143  fun needed_values_for_datatype [] _ _ = SOME []
  22.144    | needed_values_for_datatype need_us ofs
  22.145 -        ({typ, card, constrs, ...} : datatype_spec) =
  22.146 +                               ({typ, card, constrs, ...} : datatype_spec) =
  22.147      let
  22.148        fun aux (u as Construct (FreeRel (_, _, _, s) :: _, T, _, us)) =
  22.149            fold aux us
  22.150 @@ -1537,9 +1589,10 @@
  22.151        SOME (index_seq 0 card, []) |> fold aux need_us |> Option.map (rev o snd)
  22.152      end
  22.153  
  22.154 -fun needed_value_axioms_for_datatype _ _ NONE = [KK.False]
  22.155 -  | needed_value_axioms_for_datatype ofs kk (SOME fixed) =
  22.156 -    fixed |> map (atom_equation_for_nut ofs kk)
  22.157 +fun needed_value_axioms_for_datatype _ _ _ (_, NONE) = [KK.False]
  22.158 +  | needed_value_axioms_for_datatype ofs kk dtypes (T, SOME fixed) =
  22.159 +    if is_datatype_nat_like (the (datatype_spec dtypes T)) then []
  22.160 +    else fixed |> map_filter (atom_equation_for_nut ofs kk)
  22.161  
  22.162  fun all_ge ({kk_join, kk_reflexive_closure, ...} : kodkod_constrs) z r =
  22.163    kk_join r (kk_reflexive_closure (KK.Rel (suc_rel_for_atom_seq z)))
  22.164 @@ -1707,27 +1760,35 @@
  22.165             |> maps (sym_break_axioms_for_datatype hol_ctxt binarize kk rel_table
  22.166                                                    nfas dtypes)
  22.167  
  22.168 -fun sel_axiom_for_sel hol_ctxt binarize j0
  22.169 +fun sel_axioms_for_sel hol_ctxt binarize j0
  22.170          (kk as {kk_all, kk_formula_if, kk_subset, kk_no, kk_join, ...})
  22.171 -        rel_table dom_r ({const, delta, epsilon, exclusive, ...} : constr_spec)
  22.172 -        n =
  22.173 +        need_vals rel_table dom_r (dtype as {typ, ...})
  22.174 +        ({const, delta, epsilon, exclusive, ...} : constr_spec) n =
  22.175    let
  22.176      val x = binarized_and_boxed_nth_sel_for_constr hol_ctxt binarize const n
  22.177      val (r, R, _) = const_triple rel_table x
  22.178 +    val rel_x =
  22.179 +      case r of
  22.180 +        KK.Rel x => x
  22.181 +      | _ => raise BAD ("Nitpick_Kodkod.sel_axioms_for_sel", "non-Rel")
  22.182      val R2 = dest_Func R |> snd
  22.183      val z = (epsilon - delta, delta + j0)
  22.184    in
  22.185      if exclusive then
  22.186 -      kk_n_ary_function kk (Func (Atom z, R2)) r
  22.187 +      [kk_n_ary_function kk (Func (Atom z, R2)) r]
  22.188 +    else if all_values_are_needed need_vals dtype then
  22.189 +      typ |> needed_values need_vals
  22.190 +          |> filter (is_sel_of_constr rel_x)
  22.191 +          |> map (fn (_, j) => kk_n_ary_function kk R2 (kk_join (KK.Atom j) r))
  22.192      else
  22.193        let val r' = kk_join (KK.Var (1, 0)) r in
  22.194 -        kk_all [KK.DeclOne ((1, 0), KK.AtomSeq z)]
  22.195 -               (kk_formula_if (kk_subset (KK.Var (1, 0)) dom_r)
  22.196 -                              (kk_n_ary_function kk R2 r') (kk_no r'))
  22.197 +        [kk_all [KK.DeclOne ((1, 0), KK.AtomSeq z)]
  22.198 +                (kk_formula_if (kk_subset (KK.Var (1, 0)) dom_r)
  22.199 +                               (kk_n_ary_function kk R2 r') (kk_no r'))]
  22.200        end
  22.201    end
  22.202 -fun sel_axioms_for_constr hol_ctxt binarize bits j0 kk rel_table
  22.203 -        (constr as {const, delta, epsilon, explicit_max, ...}) =
  22.204 +fun sel_axioms_for_constr hol_ctxt binarize bits j0 kk need_vals rel_table
  22.205 +        dtype (constr as {const, delta, epsilon, explicit_max, ...}) =
  22.206    let
  22.207      val honors_explicit_max =
  22.208        explicit_max < 0 orelse epsilon - delta <= explicit_max
  22.209 @@ -1749,17 +1810,20 @@
  22.210                               " too small for \"max\"")
  22.211        in
  22.212          max_axiom ::
  22.213 -        map (sel_axiom_for_sel hol_ctxt binarize j0 kk rel_table dom_r constr)
  22.214 -            (index_seq 0 (num_sels_for_constr_type (snd const)))
  22.215 +        maps (sel_axioms_for_sel hol_ctxt binarize j0 kk need_vals rel_table
  22.216 +                                 dom_r dtype constr)
  22.217 +             (index_seq 0 (num_sels_for_constr_type (snd const)))
  22.218        end
  22.219    end
  22.220 -fun sel_axioms_for_datatype hol_ctxt binarize bits j0 kk rel_table
  22.221 -                            ({constrs, ...} : datatype_spec) =
  22.222 -  maps (sel_axioms_for_constr hol_ctxt binarize bits j0 kk rel_table) constrs
  22.223 +fun sel_axioms_for_datatype hol_ctxt binarize bits j0 kk rel_table need_vals
  22.224 +                            (dtype as {constrs, ...}) =
  22.225 +  maps (sel_axioms_for_constr hol_ctxt binarize bits j0 kk rel_table need_vals
  22.226 +                              dtype) constrs
  22.227  
  22.228 -fun uniqueness_axiom_for_constr hol_ctxt binarize
  22.229 +fun uniqueness_axioms_for_constr hol_ctxt binarize
  22.230          ({kk_all, kk_implies, kk_and, kk_rel_eq, kk_lone, kk_join, ...}
  22.231 -         : kodkod_constrs) rel_table ({const, ...} : constr_spec) =
  22.232 +         : kodkod_constrs) need_vals rel_table dtype
  22.233 +        ({const, ...} : constr_spec) =
  22.234    let
  22.235      fun conjunct_for_sel r =
  22.236        kk_rel_eq (kk_join (KK.Var (1, 0)) r) (kk_join (KK.Var (1, 1)) r)
  22.237 @@ -1771,36 +1835,42 @@
  22.238      val set_r = triples |> hd |> #1
  22.239    in
  22.240      if num_sels = 0 then
  22.241 -      kk_lone set_r
  22.242 +      [kk_lone set_r]
  22.243 +    else if all_values_are_needed need_vals dtype then
  22.244 +      []
  22.245      else
  22.246 -      kk_all (map (KK.DeclOne o rpair set_r o pair 1) [0, 1])
  22.247 -             (kk_implies
  22.248 -                  (fold1 kk_and (map (conjunct_for_sel o #1) (tl triples)))
  22.249 -                  (kk_rel_eq (KK.Var (1, 0)) (KK.Var (1, 1))))
  22.250 +      [kk_all (map (KK.DeclOne o rpair set_r o pair 1) [0, 1])
  22.251 +              (kk_implies
  22.252 +                   (fold1 kk_and (map (conjunct_for_sel o #1) (tl triples)))
  22.253 +                   (kk_rel_eq (KK.Var (1, 0)) (KK.Var (1, 1))))]
  22.254    end
  22.255 -fun uniqueness_axioms_for_datatype hol_ctxt binarize kk rel_table
  22.256 -                                   ({constrs, ...} : datatype_spec) =
  22.257 -  map (uniqueness_axiom_for_constr hol_ctxt binarize kk rel_table) constrs
  22.258 +fun uniqueness_axioms_for_datatype hol_ctxt binarize kk need_vals rel_table
  22.259 +                                   (dtype as {constrs, ...}) =
  22.260 +  maps (uniqueness_axioms_for_constr hol_ctxt binarize kk need_vals rel_table
  22.261 +                                     dtype) constrs
  22.262  
  22.263  fun effective_constr_max ({delta, epsilon, ...} : constr_spec) = epsilon - delta
  22.264  fun partition_axioms_for_datatype j0 (kk as {kk_rel_eq, kk_union, ...})
  22.265 -                                  rel_table
  22.266 -                                  ({card, constrs, ...} : datatype_spec) =
  22.267 +        need_vals rel_table (dtype as {card, constrs, ...}) =
  22.268    if forall #exclusive constrs then
  22.269      [Integer.sum (map effective_constr_max constrs) = card |> formula_for_bool]
  22.270 +  else if all_values_are_needed need_vals dtype then
  22.271 +    []
  22.272    else
  22.273      let val rs = map (discr_rel_expr rel_table o #const) constrs in
  22.274        [kk_rel_eq (fold1 kk_union rs) (KK.AtomSeq (card, j0)),
  22.275         kk_disjoint_sets kk rs]
  22.276      end
  22.277  
  22.278 -fun other_axioms_for_datatype _ _ _ _ _ _ {deep = false, ...} = []
  22.279 -  | other_axioms_for_datatype hol_ctxt binarize bits ofs kk rel_table
  22.280 +fun other_axioms_for_datatype _ _ _ _ _ _ _ {deep = false, ...} = []
  22.281 +  | other_axioms_for_datatype hol_ctxt binarize need_vals bits ofs kk rel_table
  22.282                                (dtype as {typ, ...}) =
  22.283      let val j0 = offset_of_type ofs typ in
  22.284 -      sel_axioms_for_datatype hol_ctxt binarize bits j0 kk rel_table dtype @
  22.285 -      uniqueness_axioms_for_datatype hol_ctxt binarize kk rel_table dtype @
  22.286 -      partition_axioms_for_datatype j0 kk rel_table dtype
  22.287 +      sel_axioms_for_datatype hol_ctxt binarize bits j0 kk need_vals rel_table
  22.288 +                              dtype @
  22.289 +      uniqueness_axioms_for_datatype hol_ctxt binarize kk need_vals rel_table
  22.290 +                                     dtype @
  22.291 +      partition_axioms_for_datatype j0 kk need_vals rel_table dtype
  22.292      end
  22.293  
  22.294  fun declarative_axioms_for_datatypes hol_ctxt binarize need_us need_vals
  22.295 @@ -1812,11 +1882,11 @@
  22.296               |> strongly_connected_sub_nfas
  22.297    in
  22.298      acyclicity_axioms_for_datatypes kk nfas @
  22.299 -    maps (needed_value_axioms_for_datatype ofs kk o snd) need_vals @
  22.300 +    maps (needed_value_axioms_for_datatype ofs kk dtypes) need_vals @
  22.301      sym_break_axioms_for_datatypes hol_ctxt binarize need_us datatype_sym_break
  22.302                                     kk rel_table nfas dtypes @
  22.303 -    maps (other_axioms_for_datatype hol_ctxt binarize bits ofs kk rel_table)
  22.304 -         dtypes
  22.305 +    maps (other_axioms_for_datatype hol_ctxt binarize need_vals bits ofs kk
  22.306 +                                    rel_table) dtypes
  22.307    end
  22.308  
  22.309  end;
    23.1 --- a/src/HOL/Tools/Predicate_Compile/mode_inference.ML	Fri Mar 18 18:19:42 2011 +0100
    23.2 +++ b/src/HOL/Tools/Predicate_Compile/mode_inference.ML	Mon Mar 21 08:29:16 2011 +0100
    23.3 @@ -527,10 +527,10 @@
    23.4      val rs = these (AList.lookup (op =) clauses p)
    23.5      fun check_mode m =
    23.6        let
    23.7 -        val res = Output.cond_timeit false "work part of check_mode for one mode" (fn _ => 
    23.8 +        val res = cond_timeit false "work part of check_mode for one mode" (fn _ => 
    23.9            map (check_mode_clause' mode_analysis_options thy p param_vs modes m) rs)
   23.10        in
   23.11 -        Output.cond_timeit false "aux part of check_mode for one mode" (fn _ => 
   23.12 +        cond_timeit false "aux part of check_mode for one mode" (fn _ => 
   23.13          case find_indices is_none res of
   23.14            [] => Success (exists (fn SOME (_, _, true) => true | _ => false) res)
   23.15          | is => (print_failed_mode options thy modes p m rs is; Error (error_of p m is)))
   23.16 @@ -538,7 +538,7 @@
   23.17      val _ = if show_mode_inference options then
   23.18          tracing ("checking " ^ string_of_int (length ms) ^ " modes ...")
   23.19        else ()
   23.20 -    val res = Output.cond_timeit false "check_mode" (fn _ => map (fn (m, _) => (m, check_mode m)) ms)
   23.21 +    val res = cond_timeit false "check_mode" (fn _ => map (fn (m, _) => (m, check_mode m)) ms)
   23.22      val (ms', errors) = split res
   23.23    in
   23.24      ((p, (ms' : ((bool * mode) * bool) list)), errors)
   23.25 @@ -622,7 +622,7 @@
   23.26        (check_modes_pred' mode_analysis_options options ctxt param_vs clauses
   23.27          (modes @ extra_modes)) modes
   23.28      val ((modes : (string * ((bool * mode) * bool) list) list), errors) =
   23.29 -      Output.cond_timeit false "Fixpount computation of mode analysis" (fn () =>
   23.30 +      cond_timeit false "Fixpount computation of mode analysis" (fn () =>
   23.31        if show_invalid_clauses options then
   23.32          fixp_with_state (fn (modes, errors) =>
   23.33            let
    24.1 --- a/src/HOL/Tools/Predicate_Compile/predicate_compile.ML	Fri Mar 18 18:19:42 2011 +0100
    24.2 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile.ML	Mon Mar 21 08:29:16 2011 +0100
    24.3 @@ -130,12 +130,12 @@
    24.4  fun preprocess options t thy =
    24.5    let
    24.6      val _ = print_step options "Fetching definitions from theory..."
    24.7 -    val gr = Output.cond_timeit (!Quickcheck.timing) "preprocess-obtain graph"
    24.8 +    val gr = cond_timeit (!Quickcheck.timing) "preprocess-obtain graph"
    24.9            (fn () => Predicate_Compile_Data.obtain_specification_graph options thy t
   24.10            |> (fn gr => Term_Graph.subgraph (member (op =) (Term_Graph.all_succs gr [t])) gr))
   24.11      val _ = if !present_graph then Predicate_Compile_Data.present_graph gr else ()
   24.12    in
   24.13 -    Output.cond_timeit (!Quickcheck.timing) "preprocess-process"
   24.14 +    cond_timeit (!Quickcheck.timing) "preprocess-process"
   24.15        (fn () => (fold_rev (preprocess_strong_conn_constnames options gr)
   24.16          (Term_Graph.strong_conn gr) thy))
   24.17    end
    25.1 --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Fri Mar 18 18:19:42 2011 +0100
    25.2 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Mon Mar 21 08:29:16 2011 +0100
    25.3 @@ -1363,7 +1363,7 @@
    25.4      val (lookup_mode, lookup_neg_mode, needs_random) = (modes_of compilation ctxt,
    25.5        modes_of (negative_compilation_of compilation) ctxt, needs_random ctxt)
    25.6      val ((moded_clauses, needs_random), errors) =
    25.7 -      Output.cond_timeit (!Quickcheck.timing) "Infering modes"
    25.8 +      cond_timeit (!Quickcheck.timing) "Infering modes"
    25.9        (fn _ => infer_modes mode_analysis_options
   25.10          options (lookup_mode, lookup_neg_mode, needs_random) ctxt preds all_modes param_vs clauses)
   25.11      val thy' = fold (fn (s, ms) => set_needs_random s ms) needs_random thy
   25.12 @@ -1373,19 +1373,19 @@
   25.13      val _ = print_modes options modes
   25.14      val _ = print_step options "Defining executable functions..."
   25.15      val thy'' =
   25.16 -      Output.cond_timeit (!Quickcheck.timing) "Defining executable functions..."
   25.17 +      cond_timeit (!Quickcheck.timing) "Defining executable functions..."
   25.18        (fn _ => fold (#define_functions (dest_steps steps) options preds) modes thy'
   25.19        |> Theory.checkpoint)
   25.20      val ctxt'' = ProofContext.init_global thy''
   25.21      val _ = print_step options "Compiling equations..."
   25.22      val compiled_terms =
   25.23 -      Output.cond_timeit (!Quickcheck.timing) "Compiling equations...." (fn _ =>
   25.24 +      cond_timeit (!Quickcheck.timing) "Compiling equations...." (fn _ =>
   25.25          compile_preds options
   25.26            (#comp_modifiers (dest_steps steps)) ctxt'' all_vs param_vs preds moded_clauses)
   25.27      val _ = print_compiled_terms options ctxt'' compiled_terms
   25.28      val _ = print_step options "Proving equations..."
   25.29      val result_thms =
   25.30 -      Output.cond_timeit (!Quickcheck.timing) "Proving equations...." (fn _ =>
   25.31 +      cond_timeit (!Quickcheck.timing) "Proving equations...." (fn _ =>
   25.32        #prove (dest_steps steps) options thy'' clauses preds moded_clauses compiled_terms)
   25.33      val result_thms' = #add_code_equations (dest_steps steps) ctxt'' preds
   25.34        (maps_modes result_thms)
   25.35 @@ -1393,7 +1393,7 @@
   25.36      val attrib = fn thy => Attrib.attribute_i thy (Attrib.internal (K (Thm.declaration_attribute
   25.37        (fn thm => Context.mapping (Code.add_eqn thm) I))))
   25.38      val thy''' =
   25.39 -      Output.cond_timeit (!Quickcheck.timing) "Setting code equations...." (fn _ =>
   25.40 +      cond_timeit (!Quickcheck.timing) "Setting code equations...." (fn _ =>
   25.41        fold (fn (name, result_thms) => fn thy => snd (Global_Theory.add_thmss
   25.42        [((Binding.qualify true (Long_Name.base_name name) (Binding.name qname), result_thms),
   25.43          [attrib thy ])] thy))
    26.1 --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_quickcheck.ML	Fri Mar 18 18:19:42 2011 +0100
    26.2 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_quickcheck.ML	Mon Mar 21 08:29:16 2011 +0100
    26.3 @@ -211,12 +211,9 @@
    26.4  
    26.5  val mk_split_lambda = HOLogic.tupled_lambda o HOLogic.mk_tuple
    26.6  
    26.7 -fun cpu_time description f =
    26.8 -  let
    26.9 -    val start = start_timing ()
   26.10 -    val result = Exn.capture f ()
   26.11 -    val time = Time.toMilliseconds (#cpu (end_timing start))
   26.12 -  in (Exn.release result, (description, time)) end
   26.13 +fun cpu_time description e =
   26.14 +  let val ({cpu, ...}, result) = Timing.timing e ()
   26.15 +  in (result, (description, Time.toMilliseconds cpu)) end
   26.16  
   26.17  fun compile_term compilation options ctxt (t, eval_terms) =
   26.18    let
    27.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML	Fri Mar 18 18:19:42 2011 +0100
    27.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML	Mon Mar 21 08:29:16 2011 +0100
    27.3 @@ -115,8 +115,8 @@
    27.4    let
    27.5      val ths = Attrib.eval_thms ctxt [xthm]
    27.6      val bracket =
    27.7 -      implode (map (fn arg => "[" ^ Pretty.str_of (Args.pretty_src ctxt arg)
    27.8 -                               ^ "]") args)
    27.9 +      map (enclose "[" "]" o Pretty.str_of o Args.pretty_src ctxt) args
   27.10 +      |> implode
   27.11      fun nth_name j =
   27.12        case xref of
   27.13          Facts.Fact s => backquote s ^ bracket
    28.1 --- a/src/HOL/Tools/try.ML	Fri Mar 18 18:19:42 2011 +0100
    28.2 +++ b/src/HOL/Tools/try.ML	Mon Mar 21 08:29:16 2011 +0100
    28.3 @@ -7,7 +7,9 @@
    28.4  signature TRY =
    28.5  sig
    28.6    val auto : bool Unsynchronized.ref
    28.7 -  val invoke_try : Time.time option -> Proof.state -> bool
    28.8 +  val invoke_try :
    28.9 +    Time.time option -> string list * string list * string list -> Proof.state
   28.10 +    -> bool
   28.11    val setup : theory -> theory
   28.12  end;
   28.13  
   28.14 @@ -40,59 +42,85 @@
   28.15        NONE
   28.16    end
   28.17  
   28.18 -fun named_method thy name =
   28.19 -  Method.method thy (Args.src ((name, []), Position.none))
   28.20 +val parse_method =
   28.21 +  enclose "(" ")"
   28.22 +  #> Outer_Syntax.scan Position.start
   28.23 +  #> filter Token.is_proper
   28.24 +  #> Scan.read Token.stopper Method.parse
   28.25 +  #> (fn SOME (Method.Source src) => src | _ => raise Fail "expected Source")
   28.26  
   28.27 -fun apply_named_method_on_first_goal name ctxt =
   28.28 -  let val thy = ProofContext.theory_of ctxt in
   28.29 -    Proof.refine (Method.SelectGoals (1, Method.Basic (named_method thy name)))
   28.30 -  end
   28.31 +fun apply_named_method_on_first_goal method thy =
   28.32 +  method |> parse_method
   28.33 +         |> Method.method thy
   28.34 +         |> Method.Basic
   28.35 +         |> curry Method.SelectGoals 1
   28.36 +         |> Proof.refine
   28.37    handle ERROR _ => K Seq.empty (* e.g., the method isn't available yet *)
   28.38  
   28.39 -fun do_named_method (name, (all_goals, run_if_auto)) auto timeout_opt st =
   28.40 +fun add_attr_text (NONE, _) s = s
   28.41 +  | add_attr_text (_, []) s = s
   28.42 +  | add_attr_text (SOME x, fs) s =
   28.43 +    s ^ " " ^ (if x = "" then "" else x ^ ": ") ^ space_implode " " fs
   28.44 +fun attrs_text (sx, ix, ex) (ss, is, es) =
   28.45 +  "" |> fold add_attr_text [(sx, ss), (ix, is), (ex, es)]
   28.46 +
   28.47 +fun do_named_method (name, ((all_goals, run_if_auto), attrs)) auto timeout_opt
   28.48 +                    triple st =
   28.49    if not auto orelse run_if_auto then
   28.50 -    do_generic timeout_opt
   28.51 -               (name ^ (if all_goals andalso
   28.52 -                           nprems_of (#goal (Proof.goal st)) > 1 then
   28.53 -                          "[1]"
   28.54 -                        else
   28.55 -                          "")) I (#goal o Proof.goal)
   28.56 -               (apply_named_method_on_first_goal name (Proof.context_of st)) st
   28.57 +    let val attrs = attrs_text attrs triple in
   28.58 +      do_generic timeout_opt
   28.59 +                 (name ^ (if all_goals andalso
   28.60 +                             nprems_of (#goal (Proof.goal st)) > 1 then
   28.61 +                            "[1]"
   28.62 +                          else
   28.63 +                            "") ^
   28.64 +                  attrs) I (#goal o Proof.goal)
   28.65 +                 (apply_named_method_on_first_goal (name ^ attrs)
   28.66 +                                                   (Proof.theory_of st)) st
   28.67 +    end
   28.68    else
   28.69      NONE
   28.70  
   28.71 -(* name * (all_goals, run_if_auto) *)
   28.72 +val full_attrs = (SOME "simp", SOME "intro", SOME "elim")
   28.73 +val clas_attrs = (NONE, SOME "intro", SOME "elim")
   28.74 +val simp_attrs = (SOME "add", NONE, NONE)
   28.75 +val metis_attrs = (SOME "", SOME "", SOME "")
   28.76 +val no_attrs = (NONE, NONE, NONE)
   28.77 +
   28.78 +(* name * ((all_goals, run_if_auto), (simp, intro, elim) *)
   28.79  val named_methods =
   28.80 -  [("simp", (false, true)),
   28.81 -   ("auto", (true, true)),
   28.82 -   ("fast", (false, false)),
   28.83 -   ("fastsimp", (false, false)),
   28.84 -   ("force", (false, false)),
   28.85 -   ("blast", (false, true)),
   28.86 -   ("metis", (false, true)),
   28.87 -   ("linarith", (false, true)),
   28.88 -   ("presburger", (false, true))]
   28.89 +  [("simp", ((false, true), simp_attrs)),
   28.90 +   ("auto", ((true, true), full_attrs)),
   28.91 +   ("fast", ((false, false), clas_attrs)),
   28.92 +   ("fastsimp", ((false, false), full_attrs)),
   28.93 +   ("force", ((false, false), full_attrs)),
   28.94 +   ("blast", ((false, true), clas_attrs)),
   28.95 +   ("metis", ((false, true), metis_attrs)),
   28.96 +   ("linarith", ((false, true), no_attrs)),
   28.97 +   ("presburger", ((false, true), no_attrs))]
   28.98  val do_methods = map do_named_method named_methods
   28.99  
  28.100  fun time_string (s, ms) = s ^ ": " ^ string_of_int ms ^ " ms"
  28.101  
  28.102 -fun do_try auto timeout_opt st =
  28.103 +fun do_try auto timeout_opt triple st =
  28.104    let
  28.105      val st = st |> Proof.map_context (Config.put Metis_Tactics.verbose false)
  28.106    in
  28.107 -    case do_methods |> Par_List.map (fn f => f auto timeout_opt st)
  28.108 +    case do_methods |> Par_List.map (fn f => f auto timeout_opt triple st)
  28.109                      |> map_filter I |> sort (int_ord o pairself snd) of
  28.110        [] => (if auto then () else writeln "No proof found."; (false, st))
  28.111      | xs as (s, _) :: _ =>
  28.112        let
  28.113 -        val xs = xs |> map swap |> AList.coalesce (op =)
  28.114 +        val xs = xs |> map (fn (s, n) => (n, hd (space_explode " " s)))
  28.115 +                    |> AList.coalesce (op =)
  28.116                      |> map (swap o apsnd commas)
  28.117 +        val need_parens = exists_string (curry (op =) " ") s
  28.118          val message =
  28.119            (if auto then "Auto Try found a proof" else "Try this command") ^
  28.120            ": " ^
  28.121            Markup.markup Markup.sendback
  28.122                ((if nprems_of (#goal (Proof.goal st)) = 1 then "by"
  28.123 -                else "apply") ^ " " ^ s) ^
  28.124 +                else "apply") ^ " " ^ (s |> need_parens ? enclose "(" ")")) ^
  28.125            "\n(" ^ space_implode "; " (map time_string xs) ^ ").\n"
  28.126        in
  28.127          (true, st |> (if auto then
  28.128 @@ -105,17 +133,43 @@
  28.129        end
  28.130    end
  28.131  
  28.132 -val invoke_try = fst oo do_try false
  28.133 +fun invoke_try timeout_opt = fst oo do_try false timeout_opt
  28.134  
  28.135  val tryN = "try"
  28.136  
  28.137 +fun try_trans triple =
  28.138 +  Toplevel.keep (K () o do_try false (SOME default_timeout) triple
  28.139 +                 o Toplevel.proof_of)
  28.140 +
  28.141 +fun merge_attrs (s1, i1, e1) (s2, i2, e2) = (s1 @ s2, i1 @ i2, e1 @ e2)
  28.142 +
  28.143 +fun string_of_xthm (xref, args) =
  28.144 +  Facts.string_of_ref xref ^
  28.145 +  implode (map (enclose "[" "]" o Pretty.str_of
  28.146 +                o Args.pretty_src @{context}) args)
  28.147 +
  28.148 +val parse_fact_refs =
  28.149 +  Scan.repeat1 (Scan.unless (Parse.name -- Args.colon)
  28.150 +                            (Parse_Spec.xthm >> string_of_xthm))
  28.151 +val parse_attr =
  28.152 +     Args.$$$ "simp" |-- Args.colon |-- parse_fact_refs
  28.153 +     >> (fn ss => (ss, [], []))
  28.154 +  || Args.$$$ "intro" |-- Args.colon |-- parse_fact_refs
  28.155 +     >> (fn is => ([], is, []))
  28.156 +  || Args.$$$ "elim" |-- Args.colon |-- parse_fact_refs
  28.157 +     >> (fn es => ([], [], es))
  28.158 +fun parse_attrs x =
  28.159 +    (Args.parens parse_attrs
  28.160 +  || Scan.repeat parse_attr
  28.161 +     >> (fn triple => fold merge_attrs triple ([], [], []))) x
  28.162 +
  28.163 +val parse_try_command = Scan.optional parse_attrs ([], [], []) #>> try_trans
  28.164 +
  28.165  val _ =
  28.166    Outer_Syntax.improper_command tryN
  28.167 -      "try a combination of proof methods" Keyword.diag
  28.168 -      (Scan.succeed (Toplevel.keep (K () o do_try false (SOME default_timeout)
  28.169 -                                    o Toplevel.proof_of)))
  28.170 +      "try a combination of proof methods" Keyword.diag parse_try_command
  28.171  
  28.172 -val auto_try = do_try true NONE
  28.173 +val auto_try = do_try true NONE ([], [], [])
  28.174  
  28.175  val setup = Auto_Tools.register_tool (auto, auto_try)
  28.176  
    29.1 --- a/src/HOL/ex/SAT_Examples.thy	Fri Mar 18 18:19:42 2011 +0100
    29.2 +++ b/src/HOL/ex/SAT_Examples.thy	Mon Mar 21 08:29:16 2011 +0100
    29.3 @@ -536,13 +536,12 @@
    29.4    fun and_to_list (Prop_Logic.And (fm1, fm2)) acc = and_to_list fm2 (fm1 :: acc)
    29.5      | and_to_list fm acc = rev (fm :: acc)
    29.6    val clauses = and_to_list prop_fm []
    29.7 -  val terms   = map (HOLogic.mk_Trueprop o Prop_Logic.term_of_prop_formula)
    29.8 -    clauses
    29.9 -  val cterms  = map (Thm.cterm_of @{theory}) terms
   29.10 -  val timer   = start_timing ()
   29.11 -  val thm     = sat.rawsat_thm @{context} cterms
   29.12 +  val terms = map (HOLogic.mk_Trueprop o Prop_Logic.term_of_prop_formula) clauses
   29.13 +  val cterms = map (Thm.cterm_of @{theory}) terms
   29.14 +  val start = Timing.start ()
   29.15 +  val thm = sat.rawsat_thm @{context} cterms
   29.16  in
   29.17 -  (end_timing timer, !sat.counter)
   29.18 +  (Timing.result start, ! sat.counter)
   29.19  end;
   29.20  *}
   29.21  
    30.1 --- a/src/Provers/blast.ML	Fri Mar 18 18:19:42 2011 +0100
    30.2 +++ b/src/Provers/blast.ML	Mon Mar 21 08:29:16 2011 +0100
    30.3 @@ -914,7 +914,7 @@
    30.4  
    30.5  fun printStats (State {ntried, nclosed, ...}) (b, start, tacs) =
    30.6    if b then
    30.7 -    writeln (#message (end_timing start) ^ " for search.  Closed: "
    30.8 +    writeln (Timing.message (Timing.result start) ^ " for search.  Closed: "
    30.9               ^ string_of_int (!nclosed) ^
   30.10               " tried: " ^ string_of_int (!ntried) ^
   30.11               " tactics: " ^ string_of_int (length tacs))
   30.12 @@ -1256,7 +1256,7 @@
   30.13        val hyps  = strip_imp_prems skoprem
   30.14        and concl = strip_imp_concl skoprem
   30.15        fun cont (tacs,_,choices) =
   30.16 -          let val start = start_timing ()
   30.17 +          let val start = Timing.start ()
   30.18            in
   30.19            case Seq.pull(EVERY' (rev tacs) i st) of
   30.20                NONE => (writeln ("PROOF FAILED for depth " ^
   30.21 @@ -1265,7 +1265,7 @@
   30.22                         else ();
   30.23                         backtrack choices)
   30.24              | cell => (if (!trace orelse !stats)
   30.25 -                       then writeln (#message (end_timing start) ^ " for reconstruction")
   30.26 +                       then writeln (Timing.message (Timing.result start) ^ " for reconstruction")
   30.27                         else ();
   30.28                         Seq.make(fn()=> cell))
   30.29            end
   30.30 @@ -1273,13 +1273,13 @@
   30.31    handle PROVE     => Seq.empty
   30.32  
   30.33  (*Public version with fixed depth*)
   30.34 -fun depth_tac cs lim i st = timing_depth_tac (start_timing ()) cs lim i st;
   30.35 +fun depth_tac cs lim i st = timing_depth_tac (Timing.start ()) cs lim i st;
   30.36  
   30.37  val (depth_limit, setup_depth_limit) = Attrib.config_int_global "blast_depth_limit" (K 20);
   30.38  
   30.39  fun blast_tac cs i st =
   30.40      ((DEEPEN (1, Config.get_global (Thm.theory_of_thm st) depth_limit)
   30.41 -        (timing_depth_tac (start_timing ()) cs) 0) i
   30.42 +        (timing_depth_tac (Timing.start ()) cs) 0) i
   30.43       THEN flexflex_tac) st
   30.44      handle TRANS s =>
   30.45        ((if !trace then warning ("blast: " ^ s) else ());
   30.46 @@ -1299,7 +1299,7 @@
   30.47    let
   30.48      val state as State {fullTrace = ft, ...} = initialize thy;
   30.49      val res = timeap prove
   30.50 -      (state, start_timing(), cs, [initBranch ([readGoal thy s], lim)], I);
   30.51 +      (state, Timing.start (), cs, [initBranch ([readGoal thy s], lim)], I);
   30.52      val _ = fullTrace := !ft;
   30.53    in res end;
   30.54  
    31.1 --- a/src/Pure/General/file.ML	Fri Mar 18 18:19:42 2011 +0100
    31.2 +++ b/src/Pure/General/file.ML	Mon Mar 21 08:29:16 2011 +0100
    31.3 @@ -11,12 +11,13 @@
    31.4    val shell_path: Path.T -> string
    31.5    val cd: Path.T -> unit
    31.6    val pwd: unit -> Path.T
    31.7 -  val full_path: Path.T -> Path.T
    31.8 +  val full_path: Path.T -> Path.T -> Path.T
    31.9    val tmp_path: Path.T -> Path.T
   31.10    val exists: Path.T -> bool
   31.11 -  val check: Path.T -> unit
   31.12    val rm: Path.T -> unit
   31.13    val is_dir: Path.T -> bool
   31.14 +  val check_dir: Path.T -> Path.T
   31.15 +  val check_file: Path.T -> Path.T
   31.16    val open_input: (TextIO.instream -> 'a) -> Path.T -> 'a
   31.17    val open_output: (TextIO.outstream -> 'a) -> Path.T -> 'a
   31.18    val open_append: (TextIO.outstream -> 'a) -> Path.T -> 'a
   31.19 @@ -51,9 +52,18 @@
   31.20  val cd = cd o platform_path;
   31.21  val pwd = Path.explode o pwd;
   31.22  
   31.23 -fun full_path path =
   31.24 -  if Path.is_absolute path then path
   31.25 -  else Path.append (pwd ()) path;
   31.26 +
   31.27 +(* full_path *)
   31.28 +
   31.29 +fun full_path dir path =
   31.30 +  let
   31.31 +    val path' = Path.expand path;
   31.32 +    val _ = Path.is_current path' andalso error "Bad file specification";
   31.33 +    val path'' = Path.append dir path';
   31.34 +  in
   31.35 +    if Path.is_absolute path'' then path''
   31.36 +    else Path.append (pwd ()) path''
   31.37 +  end;
   31.38  
   31.39  
   31.40  (* tmp_path *)
   31.41 @@ -66,15 +76,19 @@
   31.42  
   31.43  val exists = can OS.FileSys.modTime o platform_path;
   31.44  
   31.45 -fun check path =
   31.46 -  if exists path then ()
   31.47 -  else error ("No such file or directory: " ^ Path.print path);
   31.48 -
   31.49  val rm = OS.FileSys.remove o platform_path;
   31.50  
   31.51  fun is_dir path =
   31.52    the_default false (try OS.FileSys.isDir (platform_path path));
   31.53  
   31.54 +fun check_dir path =
   31.55 +  if exists path andalso is_dir path then path
   31.56 +  else error ("No such directory: " ^ Path.print path);
   31.57 +
   31.58 +fun check_file path =
   31.59 +  if exists path andalso not (is_dir path) then path
   31.60 +  else error ("No such file: " ^ Path.print path);
   31.61 +
   31.62  
   31.63  (* open files *)
   31.64  
    32.1 --- a/src/Pure/General/markup.ML	Fri Mar 18 18:19:42 2011 +0100
    32.2 +++ b/src/Pure/General/markup.ML	Mon Mar 21 08:29:16 2011 +0100
    32.3 @@ -100,7 +100,7 @@
    32.4    val elapsedN: string
    32.5    val cpuN: string
    32.6    val gcN: string
    32.7 -  val timingN: string val timing: timing -> T
    32.8 +  val timingN: string val timing: Timing.timing -> T
    32.9    val subgoalsN: string
   32.10    val proof_stateN: string val proof_state: int -> T
   32.11    val stateN: string val state: T
   32.12 @@ -312,7 +312,7 @@
   32.13  val cpuN = "cpu";
   32.14  val gcN = "gc";
   32.15  
   32.16 -fun timing ({elapsed, cpu, gc, ...}: timing) =
   32.17 +fun timing {elapsed, cpu, gc} =
   32.18    (timingN,
   32.19     [(elapsedN, Time.toString elapsed),
   32.20      (cpuN, Time.toString cpu),
    33.1 --- a/src/Pure/General/output.ML	Fri Mar 18 18:19:42 2011 +0100
    33.2 +++ b/src/Pure/General/output.ML	Mon Mar 21 08:29:16 2011 +0100
    33.3 @@ -1,7 +1,7 @@
    33.4  (*  Title:      Pure/General/output.ML
    33.5      Author:     Makarius, Hagia Maria Sion Abbey (Jerusalem)
    33.6  
    33.7 -Output channels and timing messages.
    33.8 +Isabelle output channels.
    33.9  *)
   33.10  
   33.11  signature BASIC_OUTPUT =
   33.12 @@ -10,11 +10,6 @@
   33.13    val tracing: string -> unit
   33.14    val warning: string -> unit
   33.15    val legacy_feature: string -> unit
   33.16 -  val cond_timeit: bool -> string -> (unit -> 'a) -> 'a
   33.17 -  val timeit: (unit -> 'a) -> 'a
   33.18 -  val timeap: ('a -> 'b) -> 'a -> 'b
   33.19 -  val timeap_msg: string -> ('a -> 'b) -> 'a -> 'b
   33.20 -  val timing: bool Unsynchronized.ref
   33.21  end;
   33.22  
   33.23  signature OUTPUT =
   33.24 @@ -111,31 +106,6 @@
   33.25  
   33.26  fun legacy_feature s = warning ("Legacy feature! " ^ s);
   33.27  
   33.28 -
   33.29 -
   33.30 -(** timing **)
   33.31 -
   33.32 -(*conditional timing with message*)
   33.33 -fun cond_timeit flag msg e =
   33.34 -  if flag then
   33.35 -    let
   33.36 -      val start = start_timing ();
   33.37 -      val result = Exn.capture e ();
   33.38 -      val end_msg = #message (end_timing start);
   33.39 -      val _ = warning (if msg = "" then end_msg else msg ^ "\n" ^ end_msg);
   33.40 -    in Exn.release result end
   33.41 -  else e ();
   33.42 -
   33.43 -(*unconditional timing*)
   33.44 -fun timeit e = cond_timeit true "" e;
   33.45 -
   33.46 -(*timed application function*)
   33.47 -fun timeap f x = timeit (fn () => f x);
   33.48 -fun timeap_msg msg f x = cond_timeit true msg (fn () => f x);
   33.49 -
   33.50 -(*global timing mode*)
   33.51 -val timing = Unsynchronized.ref false;
   33.52 -
   33.53  end;
   33.54  
   33.55  structure Basic_Output: BASIC_OUTPUT = Output;
    34.1 --- a/src/Pure/General/timing.ML	Fri Mar 18 18:19:42 2011 +0100
    34.2 +++ b/src/Pure/General/timing.ML	Mon Mar 21 08:29:16 2011 +0100
    34.3 @@ -4,19 +4,46 @@
    34.4  Basic support for time measurement.
    34.5  *)
    34.6  
    34.7 -val seconds = Time.fromReal;
    34.8 +signature BASIC_TIMING =
    34.9 +sig
   34.10 +  val cond_timeit: bool -> string -> (unit -> 'a) -> 'a
   34.11 +  val timeit: (unit -> 'a) -> 'a
   34.12 +  val timeap: ('a -> 'b) -> 'a -> 'b
   34.13 +  val timeap_msg: string -> ('a -> 'b) -> 'a -> 'b
   34.14 +end
   34.15  
   34.16 -fun start_timing () =
   34.17 +signature TIMING =
   34.18 +sig
   34.19 +  include BASIC_TIMING
   34.20 +  type timing = {elapsed: Time.time, cpu: Time.time, gc: Time.time}
   34.21 +  type start
   34.22 +  val start: unit -> start
   34.23 +  val result: start -> timing
   34.24 +  val timing: ('a -> 'b) -> 'a -> timing * 'b
   34.25 +  val message: timing -> string
   34.26 +end
   34.27 +
   34.28 +structure Timing: TIMING =
   34.29 +struct
   34.30 +
   34.31 +(* timer control *)
   34.32 +
   34.33 +type timing = {elapsed: Time.time, cpu: Time.time, gc: Time.time};
   34.34 +
   34.35 +abstype start = Start of
   34.36 +  Timer.real_timer * Time.time * Timer.cpu_timer *
   34.37 +    {gc: {sys: Time.time, usr: Time.time}, nongc: {sys: Time.time, usr: Time.time}}
   34.38 +with
   34.39 +
   34.40 +fun start () =
   34.41    let
   34.42      val real_timer = Timer.startRealTimer ();
   34.43      val real_time = Timer.checkRealTimer real_timer;
   34.44      val cpu_timer = Timer.startCPUTimer ();
   34.45      val cpu_times = Timer.checkCPUTimes cpu_timer;
   34.46 -  in (real_timer, real_time, cpu_timer, cpu_times) end;
   34.47 +  in Start (real_timer, real_time, cpu_timer, cpu_times) end;
   34.48  
   34.49 -type timing = {message: string, elapsed: Time.time, cpu: Time.time, gc: Time.time};
   34.50 -
   34.51 -fun end_timing (real_timer, real_time, cpu_timer, cpu_times) : timing =
   34.52 +fun result (Start (real_timer, real_time, cpu_timer, cpu_times)) =
   34.53    let
   34.54      val real_time2 = Timer.checkRealTimer real_timer;
   34.55      val {nongc = {sys, usr}, gc = {sys = gc_sys, usr = gc_usr}} = cpu_times;
   34.56 @@ -27,10 +54,41 @@
   34.57      val elapsed = real_time2 - real_time;
   34.58      val gc = gc_usr2 - gc_usr + gc_sys2 - gc_sys;
   34.59      val cpu = usr2 - usr + sys2 - sys + gc;
   34.60 +  in {elapsed = elapsed, cpu = cpu, gc = gc} end;
   34.61  
   34.62 -    val message =
   34.63 -     (toString elapsed ^ "s elapsed time, " ^
   34.64 -      toString cpu ^ "s cpu time, " ^
   34.65 -      toString gc ^ "s GC time") handle Time.Time => "";
   34.66 -  in {message = message, elapsed = elapsed, cpu = cpu, gc = gc} end;
   34.67 +end;
   34.68 +
   34.69 +fun timing f x =
   34.70 +  let
   34.71 +    val start = start ();
   34.72 +    val y = f x;
   34.73 +  in (result start, y) end;
   34.74 +
   34.75 +
   34.76 +(* timing messages *)
   34.77 +
   34.78 +fun message {elapsed, cpu, gc} =
   34.79 +  Time.toString elapsed ^ "s elapsed time, " ^
   34.80 +  Time.toString cpu ^ "s cpu time, " ^
   34.81 +  Time.toString gc ^ "s GC time" handle Time.Time => "";
   34.82  
   34.83 +fun cond_timeit enabled msg e =
   34.84 +  if enabled then
   34.85 +    let
   34.86 +      val (timing, result) = timing (Exn.capture e) ();
   34.87 +      val end_msg = message timing;
   34.88 +      val _ =
   34.89 +        if Exn.is_interrupt_exn result then ()
   34.90 +        else warning (if msg = "" then end_msg else msg ^ "\n" ^ end_msg);
   34.91 +    in Exn.release result end
   34.92 +  else e ();
   34.93 +
   34.94 +fun timeit e = cond_timeit true "" e;
   34.95 +fun timeap f x = timeit (fn () => f x);
   34.96 +fun timeap_msg msg f x = cond_timeit true msg (fn () => f x);
   34.97 +
   34.98 +end;
   34.99 +
  34.100 +structure Basic_Timing: BASIC_TIMING = Timing;
  34.101 +open Basic_Timing;
  34.102 +
    35.1 --- a/src/Pure/IsaMakefile	Fri Mar 18 18:19:42 2011 +0100
    35.2 +++ b/src/Pure/IsaMakefile	Mon Mar 21 08:29:16 2011 +0100
    35.3 @@ -21,7 +21,6 @@
    35.4  
    35.5  BOOTSTRAP_FILES = 					\
    35.6    General/exn.ML					\
    35.7 -  General/timing.ML					\
    35.8    ML-Systems/compiler_polyml-5.2.ML			\
    35.9    ML-Systems/compiler_polyml-5.3.ML			\
   35.10    ML-Systems/ml_name_space.ML				\
   35.11 @@ -101,6 +100,7 @@
   35.12    General/symbol.ML					\
   35.13    General/symbol_pos.ML					\
   35.14    General/table.ML					\
   35.15 +  General/timing.ML					\
   35.16    General/url.ML					\
   35.17    General/xml.ML					\
   35.18    General/xml_data.ML					\
    36.1 --- a/src/Pure/Isar/outer_syntax.ML	Fri Mar 18 18:19:42 2011 +0100
    36.2 +++ b/src/Pure/Isar/outer_syntax.ML	Mon Mar 21 08:29:16 2011 +0100
    36.3 @@ -271,7 +271,7 @@
    36.4  fun load_thy name init pos text =
    36.5    let
    36.6      val (lexs, commands) = get_syntax ();
    36.7 -    val time = ! Output.timing;
    36.8 +    val time = ! Toplevel.timing;
    36.9  
   36.10      val _ = Present.init_theory name;
   36.11  
    37.1 --- a/src/Pure/Isar/toplevel.ML	Fri Mar 18 18:19:42 2011 +0100
    37.2 +++ b/src/Pure/Isar/toplevel.ML	Mon Mar 21 08:29:16 2011 +0100
    37.3 @@ -218,7 +218,7 @@
    37.4  val quiet = Unsynchronized.ref false;
    37.5  val debug = Runtime.debug;
    37.6  val interact = Unsynchronized.ref false;
    37.7 -val timing = Output.timing;
    37.8 +val timing = Unsynchronized.ref false;
    37.9  val profiling = Unsynchronized.ref 0;
   37.10  val skip_proofs = Unsynchronized.ref false;
   37.11  
    38.1 --- a/src/Pure/ML-Systems/polyml_common.ML	Fri Mar 18 18:19:42 2011 +0100
    38.2 +++ b/src/Pure/ML-Systems/polyml_common.ML	Mon Mar 21 08:29:16 2011 +0100
    38.3 @@ -14,10 +14,12 @@
    38.4  else use "ML-Systems/single_assignment_polyml.ML";
    38.5  
    38.6  use "ML-Systems/multithreading.ML";
    38.7 -use "General/timing.ML";
    38.8  use "ML-Systems/ml_pretty.ML";
    38.9  use "ML-Systems/use_context.ML";
   38.10  
   38.11 +val seconds = Time.fromReal;
   38.12 +
   38.13 +
   38.14  
   38.15  (** ML system and platform related **)
   38.16  
    39.1 --- a/src/Pure/ML-Systems/proper_int.ML	Fri Mar 18 18:19:42 2011 +0100
    39.2 +++ b/src/Pure/ML-Systems/proper_int.ML	Mon Mar 21 08:29:16 2011 +0100
    39.3 @@ -13,8 +13,6 @@
    39.4  
    39.5  (* Int *)
    39.6  
    39.7 -structure OrigInt = Int;
    39.8 -structure OrigIntInf = IntInf;
    39.9  type int = IntInf.int;
   39.10  
   39.11  structure IntInf =
    40.1 --- a/src/Pure/ML-Systems/smlnj.ML	Fri Mar 18 18:19:42 2011 +0100
    40.2 +++ b/src/Pure/ML-Systems/smlnj.ML	Mon Mar 21 08:29:16 2011 +0100
    40.3 @@ -13,7 +13,6 @@
    40.4  use "ML-Systems/universal.ML";
    40.5  use "ML-Systems/thread_dummy.ML";
    40.6  use "ML-Systems/multithreading.ML";
    40.7 -use "General/timing.ML";
    40.8  use "ML-Systems/ml_name_space.ML";
    40.9  use "ML-Systems/ml_pretty.ML";
   40.10  structure PolyML = struct end;
   40.11 @@ -21,8 +20,9 @@
   40.12  use "ML-Systems/use_context.ML";
   40.13  
   40.14  
   40.15 +val seconds = Time.fromReal;
   40.16 +
   40.17  (*low-level pointer equality*)
   40.18 -
   40.19  CM.autoload "$smlnj/init/init.cmi";
   40.20  val pointer_eq = InlineT.ptreql;
   40.21  
    41.1 --- a/src/Pure/PIDE/document.ML	Fri Mar 18 18:19:42 2011 +0100
    41.2 +++ b/src/Pure/PIDE/document.ML	Mon Mar 21 08:29:16 2011 +0100
    41.3 @@ -241,9 +241,9 @@
    41.4          val is_proof = Keyword.is_proof (Toplevel.name_of tr);
    41.5          val do_print = not is_init andalso (Toplevel.print_of tr orelse is_proof);
    41.6  
    41.7 -        val start = start_timing ();
    41.8 +        val start = Timing.start ();
    41.9          val (errs, result) = run (is_init orelse is_proof) (Toplevel.set_print false tr) st;
   41.10 -        val _ = timing tr (end_timing start);
   41.11 +        val _ = timing tr (Timing.result start);
   41.12          val _ = List.app (Toplevel.error_msg tr) errs;
   41.13          val res =
   41.14            (case result of
    42.1 --- a/src/Pure/ProofGeneral/pgip_types.ML	Fri Mar 18 18:19:42 2011 +0100
    42.2 +++ b/src/Pure/ProofGeneral/pgip_types.ML	Mon Mar 21 08:29:16 2011 +0100
    42.3 @@ -364,7 +364,9 @@
    42.4  
    42.5  fun string_of_pgipurl p = Path.implode p
    42.6  
    42.7 -fun attrval_of_pgipurl purl = "file:" ^ (XML.text (File.platform_path (File.full_path purl)))
    42.8 +fun attrval_of_pgipurl purl =
    42.9 +  "file:" ^ XML.text (File.platform_path (File.full_path Path.current purl))
   42.10 +
   42.11  fun attrs_of_pgipurl purl = [("url", attrval_of_pgipurl purl)]
   42.12  
   42.13  val pgipurl_of_attrs = pgipurl_of_string o get_attr "url"
    43.1 --- a/src/Pure/ProofGeneral/preferences.ML	Fri Mar 18 18:19:42 2011 +0100
    43.2 +++ b/src/Pure/ProofGeneral/preferences.ML	Mon Mar 21 08:29:16 2011 +0100
    43.3 @@ -156,7 +156,7 @@
    43.4    bool_pref Pattern.trace_unify_fail
    43.5      "trace-unification"
    43.6      "Output error diagnostics during unification",
    43.7 -  bool_pref Output.timing
    43.8 +  bool_pref Toplevel.timing
    43.9      "global-timing"
   43.10      "Whether to enable timing in Isabelle.",
   43.11    bool_pref Toplevel.debug
    44.1 --- a/src/Pure/ProofGeneral/proof_general_pgip.ML	Fri Mar 18 18:19:42 2011 +0100
    44.2 +++ b/src/Pure/ProofGeneral/proof_general_pgip.ML	Mon Mar 21 08:29:16 2011 +0100
    44.3 @@ -588,14 +588,14 @@
    44.4  
    44.5          fun filerefs f =
    44.6              let val thy = thy_name f
    44.7 -                val filerefs = #uses (Thy_Load.deps_thy (Path.dir f) thy)
    44.8 +                val filerefs = map #1 (#uses (Thy_Load.check_thy (Path.dir f) thy))
    44.9              in
   44.10                  issue_pgip (Setrefs {url=url, thyname=NONE, objtype=SOME PgipTypes.ObjFile,
   44.11                                       name=NONE, idtables=[], fileurls=filerefs})
   44.12              end
   44.13  
   44.14          fun thyrefs thy =
   44.15 -            let val thyrefs = #imports (Thy_Load.deps_thy Path.current thy)
   44.16 +            let val thyrefs = #imports (Thy_Load.check_thy Path.current thy)
   44.17              in
   44.18                  issue_pgip (Setrefs {url=url, thyname=thyname, objtype=SOME PgipTypes.ObjTheory,
   44.19                                       name=NONE, idtables=[{context=NONE, objtype=PgipTypes.ObjTheory,
    45.1 --- a/src/Pure/ROOT.ML	Fri Mar 18 18:19:42 2011 +0100
    45.2 +++ b/src/Pure/ROOT.ML	Mon Mar 21 08:29:16 2011 +0100
    45.3 @@ -21,6 +21,7 @@
    45.4  use "General/alist.ML";
    45.5  use "General/table.ML";
    45.6  use "General/output.ML";
    45.7 +use "General/timing.ML";
    45.8  use "General/properties.ML";
    45.9  use "General/markup.ML";
   45.10  use "General/scan.ML";
    46.1 --- a/src/Pure/System/session.ML	Fri Mar 18 18:19:42 2011 +0100
    46.2 +++ b/src/Pure/System/session.ML	Mon Mar 21 08:29:16 2011 +0100
    46.3 @@ -92,22 +92,21 @@
    46.4  fun dumping (_, "") = NONE
    46.5    | dumping (cp, path) = SOME (cp, Path.explode path);
    46.6  
    46.7 -fun use_dir item root build modes reset info doc doc_graph doc_versions parent
    46.8 +fun use_dir item root build modes reset info doc doc_graph doc_variants parent
    46.9      name dump rpath level timing verbose max_threads trace_threads
   46.10      parallel_proofs parallel_proofs_threshold =
   46.11    ((fn () =>
   46.12       (init reset parent name;
   46.13 -      Present.init build info doc doc_graph doc_versions (path ()) name
   46.14 +      Present.init build info doc doc_graph doc_variants (path ()) name
   46.15          (dumping dump) (get_rpath rpath) verbose (map Thy_Info.get_theory (Thy_Info.get_names ()));
   46.16        if timing then
   46.17          let
   46.18 -          val start = start_timing ();
   46.19 +          val start = Timing.start ();
   46.20            val _ = use root;
   46.21 -          val stop = end_timing start;
   46.22            val _ =
   46.23              Output.raw_stderr ("Timing " ^ item ^ " (" ^
   46.24                string_of_int (Multithreading.max_threads_value ()) ^ " threads, " ^
   46.25 -              #message stop ^ ")\n");
   46.26 +              Timing.message (Timing.result start) ^ ")\n");
   46.27          in () end
   46.28        else use root;
   46.29        finish ()))
    47.1 --- a/src/Pure/Thy/present.ML	Fri Mar 18 18:19:42 2011 +0100
    47.2 +++ b/src/Pure/Thy/present.ML	Mon Mar 21 08:29:16 2011 +0100
    47.3 @@ -6,7 +6,7 @@
    47.4  
    47.5  signature BASIC_PRESENT =
    47.6  sig
    47.7 -  val no_document: ('a -> 'b) -> 'a -> 'b
    47.8 +  val no_document: ('a -> 'b) -> 'a -> 'b  (*not thread-safe!*)
    47.9  end;
   47.10  
   47.11  signature PRESENT =
   47.12 @@ -18,8 +18,9 @@
   47.13    val display_graph: {name: string, ID: string, dir: string, unfold: bool,
   47.14     path: string, parents: string list} list -> unit
   47.15    val init: bool -> bool -> string -> bool -> string list -> string list ->
   47.16 -    string -> (bool * Path.T) option -> Url.T option * bool -> bool -> theory list -> unit
   47.17 -  val finish: unit -> unit
   47.18 +    string -> (bool * Path.T) option -> Url.T option * bool -> bool ->
   47.19 +    theory list -> unit  (*not thread-safe!*)
   47.20 +  val finish: unit -> unit  (*not thread-safe!*)
   47.21    val init_theory: string -> unit
   47.22    val theory_source: string -> (unit -> HTML.text) -> unit
   47.23    val theory_output: string -> string -> unit
   47.24 @@ -64,7 +65,7 @@
   47.25  
   47.26  (** additional theory data **)
   47.27  
   47.28 -structure BrowserInfoData = Theory_Data
   47.29 +structure Browser_Info = Theory_Data
   47.30  (
   47.31    type T = {name: string, session: string list, is_local: bool};
   47.32    val empty = {name = "", session = [], is_local = false}: T;
   47.33 @@ -72,8 +73,8 @@
   47.34    fun merge _ = empty;
   47.35  );
   47.36  
   47.37 -val put_info = BrowserInfoData.put;
   47.38 -val get_info = BrowserInfoData.get;
   47.39 +val put_info = Browser_Info.put;
   47.40 +val get_info = Browser_Info.get;
   47.41  val session_name = #name o get_info;
   47.42  
   47.43  
   47.44 @@ -107,7 +108,6 @@
   47.45    let
   47.46      val name = Context.theory_name thy;
   47.47      val {name = sess_name, session, is_local} = get_info thy;
   47.48 -    val path' = Path.append (Path.make session) (html_path name);
   47.49      val entry =
   47.50       {name = name, ID = ID_of session name, dir = sess_name,
   47.51        path =
   47.52 @@ -165,14 +165,14 @@
   47.53    CRITICAL (fn () => Unsynchronized.change browser_info (map_browser_info f));
   47.54  
   47.55  val suppress_tex_source = Unsynchronized.ref false;
   47.56 -fun no_document f x = Unsynchronized.setmp suppress_tex_source true f x;  (* FIXME unreliable *)
   47.57 +fun no_document f x = Unsynchronized.setmp suppress_tex_source true f x;
   47.58  
   47.59  fun init_theory_info name info =
   47.60    change_browser_info (fn (theories, files, tex_index, html_index, graph) =>
   47.61      (Symtab.update (name, info) theories, files, tex_index, html_index, graph));
   47.62  
   47.63  fun change_theory_info name f =
   47.64 -  change_browser_info (fn (info as (theories, files, tex_index, html_index, graph)) =>
   47.65 +  change_browser_info (fn (theories, files, tex_index, html_index, graph) =>
   47.66      (case Symtab.lookup theories name of
   47.67        NONE => error ("Browser info: cannot access theory document " ^ quote name)
   47.68      | SOME info => (Symtab.update (name, map_theory_info f info) theories, files,
   47.69 @@ -203,9 +203,6 @@
   47.70  fun add_html_source name txt = change_theory_info name (fn (tex_source, html_source, html) =>
   47.71    (tex_source, Buffer.add txt html_source, html));
   47.72  
   47.73 -fun add_html name txt = change_theory_info name (fn (tex_source, html_source, html) =>
   47.74 -  (tex_source, html_source, Buffer.add txt html));
   47.75 -
   47.76  
   47.77  
   47.78  (** global session state **)
   47.79 @@ -215,16 +212,16 @@
   47.80  type session_info =
   47.81    {name: string, parent: string, session: string, path: string list, html_prefix: Path.T,
   47.82      info: bool, doc_format: string, doc_graph: bool, documents: (string * string) list,
   47.83 -    doc_prefix1: (Path.T * Path.T) option, doc_prefix2: (bool * Path.T) option,
   47.84 -    remote_path: Url.T option, verbose: bool, readme: Path.T option};
   47.85 +    dump_prefix: (bool * Path.T) option, remote_path: Url.T option, verbose: bool,
   47.86 +    readme: Path.T option};
   47.87  
   47.88  fun make_session_info
   47.89    (name, parent, session, path, html_prefix, info, doc_format, doc_graph, documents,
   47.90 -    doc_prefix1, doc_prefix2, remote_path, verbose, readme) =
   47.91 +    dump_prefix, remote_path, verbose, readme) =
   47.92    {name = name, parent = parent, session = session, path = path, html_prefix = html_prefix,
   47.93      info = info, doc_format = doc_format, doc_graph = doc_graph, documents = documents,
   47.94 -    doc_prefix1 = doc_prefix1, doc_prefix2 = doc_prefix2, remote_path = remote_path,
   47.95 -    verbose = verbose, readme = readme}: session_info;
   47.96 +    dump_prefix = dump_prefix, remote_path = remote_path, verbose = verbose,
   47.97 +    readme = readme}: session_info;
   47.98  
   47.99  
  47.100  (* state *)
  47.101 @@ -232,7 +229,6 @@
  47.102  val session_info = Unsynchronized.ref (NONE: session_info option);
  47.103  
  47.104  fun with_session x f = (case ! session_info of NONE => x | SOME info => f info);
  47.105 -fun with_context f = f (Context.theory_name (ML_Context.the_global_context ()));
  47.106  
  47.107  
  47.108  
  47.109 @@ -256,22 +252,22 @@
  47.110      session_entries (get_entries dir) ^ HTML.end_document
  47.111    |> File.write (Path.append dir index_path);
  47.112  
  47.113 -fun update_index dir name = CRITICAL (fn () =>
  47.114 +fun update_index dir name =
  47.115    (case try get_entries dir of
  47.116      NONE => warning ("Browser info: cannot access session index of " ^ Path.print dir)
  47.117 -  | SOME es => (put_entries ((remove (op =) name es) @ [name]) dir; create_index dir)));
  47.118 +  | SOME es => (put_entries ((remove (op =) name es) @ [name]) dir; create_index dir));
  47.119  
  47.120  
  47.121 -(* document versions *)
  47.122 +(* document variants *)
  47.123  
  47.124 -fun read_version str =
  47.125 +fun read_variant str =
  47.126    (case space_explode "=" str of
  47.127      [name] => (name, "")
  47.128    | [name, tags] => (name, tags)
  47.129 -  | _ => error ("Malformed document version specification: " ^ quote str));
  47.130 +  | _ => error ("Malformed document variant specification: " ^ quote str));
  47.131  
  47.132 -fun read_versions strs =
  47.133 -  rev (distinct (eq_fst (op =)) (rev ((documentN, "") :: map read_version strs)))
  47.134 +fun read_variants strs =
  47.135 +  rev (distinct (eq_fst (op =)) (rev ((documentN, "") :: map read_variant strs)))
  47.136    |> filter_out (fn (_, s) => s = "-");
  47.137  
  47.138  
  47.139 @@ -279,9 +275,9 @@
  47.140  
  47.141  fun name_of_session elems = space_implode "/" ("Isabelle" :: elems);
  47.142  
  47.143 -fun init build info doc doc_graph doc_versions path name doc_prefix2
  47.144 -    (remote_path, first_time) verbose thys = CRITICAL (fn () =>
  47.145 -  if not build andalso not info andalso doc = "" andalso is_none doc_prefix2 then
  47.146 +fun init build info doc doc_graph doc_variants path name dump_prefix
  47.147 +    (remote_path, first_time) verbose thys =
  47.148 +  if not build andalso not info andalso doc = "" andalso is_none dump_prefix then
  47.149      (browser_info := empty_browser_info; session_info := NONE)
  47.150    else
  47.151      let
  47.152 @@ -290,16 +286,15 @@
  47.153        val sess_prefix = Path.make path;
  47.154        val html_prefix = Path.append (Path.expand output_path) sess_prefix;
  47.155  
  47.156 -      val (doc_prefix1, documents) =
  47.157 -        if doc = "" then (NONE, [])
  47.158 -        else if not (File.exists document_path) then
  47.159 -          (if verbose then Output.raw_stderr "Warning: missing document directory\n" else ();
  47.160 -            (NONE, []))
  47.161 -        else (SOME (Path.append html_prefix document_path, html_prefix),
  47.162 -          read_versions doc_versions);
  47.163 +      val documents =
  47.164 +        if doc = "" then []
  47.165 +        else if not (can File.check_dir document_path) then
  47.166 +          (if verbose then Output.raw_stderr "Warning: missing document directory\n" else (); [])
  47.167 +        else read_variants doc_variants;
  47.168  
  47.169        val parent_index_path = Path.append Path.parent index_path;
  47.170 -      val index_up_lnk = if first_time then
  47.171 +      val index_up_lnk =
  47.172 +        if first_time then
  47.173            Url.append (the remote_path) (Url.File (Path.append sess_prefix parent_index_path))
  47.174          else Url.File parent_index_path;
  47.175        val readme =
  47.176 @@ -309,15 +304,16 @@
  47.177  
  47.178        val docs =
  47.179          (case readme of NONE => [] | SOME p => [(Url.File p, "README")]) @
  47.180 -        map (fn (name, _) => (Url.File (Path.ext doc (Path.basic name)), name)) documents;
  47.181 +          map (fn (name, _) => (Url.File (Path.ext doc (Path.basic name)), name)) documents;
  47.182        val index_text = HTML.begin_index (index_up_lnk, parent_name)
  47.183          (Url.File index_path, session_name) docs (Url.explode "medium.html");
  47.184      in
  47.185 -      session_info := SOME (make_session_info (name, parent_name, session_name, path, html_prefix,
  47.186 -      info, doc, doc_graph, documents, doc_prefix1, doc_prefix2, remote_path, verbose, readme));
  47.187 +      session_info :=
  47.188 +        SOME (make_session_info (name, parent_name, session_name, path, html_prefix,
  47.189 +          info, doc, doc_graph, documents, dump_prefix, remote_path, verbose, readme));
  47.190        browser_info := init_browser_info remote_path path thys;
  47.191        add_html_index (0, index_text)
  47.192 -    end);
  47.193 +    end;
  47.194  
  47.195  
  47.196  (* isabelle tool wrappers *)
  47.197 @@ -365,9 +361,9 @@
  47.198    write_tex (index_buffer tex_index |> Buffer.add Latex.tex_trailer) doc_indexN path;
  47.199  
  47.200  
  47.201 -fun finish () = CRITICAL (fn () =>
  47.202 -    with_session () (fn {name, info, html_prefix, doc_format, doc_graph,
  47.203 -      documents, doc_prefix1, doc_prefix2, path, verbose, readme, ...} =>
  47.204 +fun finish () =
  47.205 +  with_session () (fn {name, info, html_prefix, doc_format,
  47.206 +    doc_graph, documents, dump_prefix, path, verbose, readme, ...} =>
  47.207    let
  47.208      val {theories, files, tex_index, html_index, graph} = ! browser_info;
  47.209      val thys = Symtab.dest theories;
  47.210 @@ -379,7 +375,7 @@
  47.211  
  47.212      val sorted_graph = sorted_index graph;
  47.213      val opt_graphs =
  47.214 -      if doc_graph andalso (is_some doc_prefix1 orelse is_some doc_prefix2) then
  47.215 +      if doc_graph andalso (not (null documents) orelse is_some dump_prefix) then
  47.216          SOME (isabelle_browser sorted_graph)
  47.217        else NONE;
  47.218  
  47.219 @@ -393,41 +389,46 @@
  47.220            File.write (Path.append path graph_eps_path) eps));
  47.221        write_tex_index tex_index path;
  47.222        List.app (finish_tex path) thys);
  47.223 +    val _ =
  47.224 +      if info then
  47.225 +       (Isabelle_System.mkdirs (Path.append html_prefix session_path);
  47.226 +        File.write_buffer (Path.append html_prefix pre_index_path) (index_buffer html_index);
  47.227 +        File.write (Path.append html_prefix session_entries_path) "";
  47.228 +        create_index html_prefix;
  47.229 +        if length path > 1 then update_index parent_html_prefix name else ();
  47.230 +        (case readme of NONE => () | SOME path => File.copy path html_prefix);
  47.231 +        write_graph sorted_graph (Path.append html_prefix graph_path);
  47.232 +        Isabelle_System.isabelle_tool "browser" "-b";
  47.233 +        File.copy (Path.explode "~~/lib/browser/GraphBrowser.jar") html_prefix;
  47.234 +        List.app (fn (a, txt) => File.write (Path.append html_prefix (Path.basic a)) txt)
  47.235 +          (HTML.applet_pages name (Url.File index_path, name));
  47.236 +        File.copy (Path.explode "~~/lib/html/isabelle.css") html_prefix;
  47.237 +        List.app finish_html thys;
  47.238 +        List.app (uncurry File.write) files;
  47.239 +        if verbose then Output.raw_stderr ("Browser info at " ^ show_path html_prefix ^ "\n")
  47.240 +        else ())
  47.241 +      else ();
  47.242 +
  47.243 +    val _ =
  47.244 +      (case dump_prefix of NONE => () | SOME (cp, path) =>
  47.245 +       (prepare_sources cp path;
  47.246 +        if verbose then Output.raw_stderr ("Document sources at " ^ show_path path ^ "\n")
  47.247 +        else ()));
  47.248 +
  47.249 +    val doc_paths =
  47.250 +      documents |> Par_List.map (fn (name, tags) =>
  47.251 +        let
  47.252 +          val path = Path.append html_prefix (Path.basic name);
  47.253 +          val _ = prepare_sources true path;
  47.254 +        in isabelle_document true doc_format name tags path html_prefix end);
  47.255 +    val _ =
  47.256 +      if verbose then
  47.257 +        doc_paths |> List.app (fn doc => Output.raw_stderr ("Document at " ^ show_path doc ^ "\n"))
  47.258 +      else ();
  47.259    in
  47.260 -    if info then
  47.261 -     (Isabelle_System.mkdirs (Path.append html_prefix session_path);
  47.262 -      File.write_buffer (Path.append html_prefix pre_index_path) (index_buffer html_index);
  47.263 -      File.write (Path.append html_prefix session_entries_path) "";
  47.264 -      create_index html_prefix;
  47.265 -      if length path > 1 then update_index parent_html_prefix name else ();
  47.266 -      (case readme of NONE => () | SOME path => File.copy path html_prefix);
  47.267 -      write_graph sorted_graph (Path.append html_prefix graph_path);
  47.268 -      Isabelle_System.isabelle_tool "browser" "-b";
  47.269 -      File.copy (Path.explode "~~/lib/browser/GraphBrowser.jar") html_prefix;
  47.270 -      List.app (fn (a, txt) => File.write (Path.append html_prefix (Path.basic a)) txt)
  47.271 -        (HTML.applet_pages name (Url.File index_path, name));
  47.272 -      File.copy (Path.explode "~~/lib/html/isabelle.css") html_prefix;
  47.273 -      List.app finish_html thys;
  47.274 -      List.app (uncurry File.write) files;
  47.275 -      if verbose then Output.raw_stderr ("Browser info at " ^ show_path html_prefix ^ "\n") else ())
  47.276 -    else ();
  47.277 -
  47.278 -    (case doc_prefix2 of NONE => () | SOME (cp, path) =>
  47.279 -     (prepare_sources cp path;
  47.280 -      if verbose then Output.raw_stderr ("Document sources at " ^ show_path path ^ "\n") else ()));
  47.281 -
  47.282 -    (case doc_prefix1 of NONE => () | SOME (path, result_path) =>
  47.283 -      documents |> List.app (fn (name, tags) =>
  47.284 -       let
  47.285 -         val _ = prepare_sources true path;
  47.286 -         val doc_path = isabelle_document true doc_format name tags path result_path;
  47.287 -       in
  47.288 -         if verbose then Output.raw_stderr ("Document at " ^ show_path doc_path ^ "\n") else ()
  47.289 -       end));
  47.290 -
  47.291      browser_info := empty_browser_info;
  47.292      session_info := NONE
  47.293 -  end));
  47.294 +  end);
  47.295  
  47.296  
  47.297  (* theory elements *)
  47.298 @@ -462,7 +463,7 @@
  47.299  
  47.300      val files_html = files |> map (fn (raw_path, loadit) =>
  47.301        let
  47.302 -        val path = #1 (Thy_Load.check_file dir raw_path);
  47.303 +        val path = Thy_Load.check_file dir raw_path;
  47.304          val base = Path.base path;
  47.305          val base_html = html_ext base;
  47.306          val _ = add_file (Path.append html_prefix base_html,
    48.1 --- a/src/Pure/Thy/term_style.ML	Fri Mar 18 18:19:42 2011 +0100
    48.2 +++ b/src/Pure/Thy/term_style.ML	Mon Mar 21 08:29:16 2011 +0100
    48.3 @@ -19,7 +19,7 @@
    48.4  fun err_dup_style name =
    48.5    error ("Duplicate declaration of antiquote style: " ^ quote name);
    48.6  
    48.7 -structure StyleData = Theory_Data
    48.8 +structure Styles = Theory_Data
    48.9  (
   48.10    type T = ((Proof.context -> term -> term) parser * stamp) Symtab.table;
   48.11    val empty = Symtab.empty;
   48.12 @@ -32,12 +32,12 @@
   48.13  (* accessors *)
   48.14  
   48.15  fun the_style thy name =
   48.16 -  (case Symtab.lookup (StyleData.get thy) name of
   48.17 +  (case Symtab.lookup (Styles.get thy) name of
   48.18      NONE => error ("Unknown antiquote style: " ^ quote name)
   48.19    | SOME (style, _) => style);
   48.20  
   48.21  fun setup name style thy =
   48.22 -  StyleData.map (Symtab.update_new (name, (style, stamp ()))) thy
   48.23 +  Styles.map (Symtab.update_new (name, (style, stamp ()))) thy
   48.24      handle Symtab.DUP _ => err_dup_style name;
   48.25  
   48.26  
    49.1 --- a/src/Pure/Thy/thy_header.ML	Fri Mar 18 18:19:42 2011 +0100
    49.2 +++ b/src/Pure/Thy/thy_header.ML	Mon Mar 21 08:29:16 2011 +0100
    49.3 @@ -7,7 +7,7 @@
    49.4  signature THY_HEADER =
    49.5  sig
    49.6    val args: Token.T list -> (string * string list * (string * bool) list) * Token.T list
    49.7 -  val read: Position.T -> string -> string * string list * (string * bool) list
    49.8 +  val read: Position.T -> string -> string * string list * (Path.T * bool) list
    49.9    val thy_path: string -> Path.T
   49.10    val split_thy_path: Path.T -> Path.T * string
   49.11    val consistent_name: string -> string -> unit
   49.12 @@ -63,7 +63,8 @@
   49.13      |> Source.source Token.stopper (Scan.single (Scan.error (Parse.!!! header))) NONE
   49.14      |> Source.get_single;
   49.15    in
   49.16 -    (case res of SOME (x, _) => x
   49.17 +    (case res of
   49.18 +      SOME ((name, imports, uses), _) => (name, imports, map (apfst Path.explode) uses)
   49.19      | NONE => error ("Unexpected end of input" ^ Position.str_of pos))
   49.20    end;
   49.21  
    50.1 --- a/src/Pure/Thy/thy_info.ML	Fri Mar 18 18:19:42 2011 +0100
    50.2 +++ b/src/Pure/Thy/thy_info.ML	Mon Mar 21 08:29:16 2011 +0100
    50.3 @@ -232,7 +232,7 @@
    50.4      val {master = (thy_path, _), imports} = deps;
    50.5      val dir = Path.dir thy_path;
    50.6      val pos = Path.position thy_path;
    50.7 -    val uses = map (apfst Path.explode) (#3 (Thy_Header.read pos text));
    50.8 +    val (_, _, uses) = Thy_Header.read pos text;
    50.9      fun init _ =
   50.10        Thy_Load.begin_theory dir name imports parent_thys uses
   50.11        |> Present.begin_theory update_time dir uses;
   50.12 @@ -251,24 +251,20 @@
   50.13  
   50.14  fun check_deps dir name =
   50.15    (case lookup_deps name of
   50.16 -    SOME NONE => (true, NONE, get_parents name, NONE)
   50.17 +    SOME NONE => (true, NONE, get_parents name)
   50.18    | NONE =>
   50.19 -      let val {master, text, imports, ...} = Thy_Load.deps_thy dir name
   50.20 -      in (false, SOME (make_deps master imports), imports, SOME text) end
   50.21 +      let val {master, text, imports, ...} = Thy_Load.check_thy dir name
   50.22 +      in (false, SOME (make_deps master imports, text), imports) end
   50.23    | SOME (SOME {master, imports}) =>
   50.24 -      let val master' = Thy_Load.check_thy dir name in
   50.25 -        if #2 master <> #2 master' then
   50.26 -          let val {text = text', imports = imports', ...} = Thy_Load.deps_thy dir name;
   50.27 -          in (false, SOME (make_deps master' imports'), imports', SOME text') end
   50.28 -        else
   50.29 -          let
   50.30 -            val current =
   50.31 -              (case lookup_theory name of
   50.32 -                NONE => false
   50.33 -              | SOME theory => Thy_Load.all_current theory);
   50.34 -            val deps' = SOME (make_deps master' imports);
   50.35 -          in (current, deps', imports, NONE) end
   50.36 -      end);
   50.37 +      let
   50.38 +        val {master = master', text = text', imports = imports', ...} = Thy_Load.check_thy dir name;
   50.39 +        val deps' = SOME (make_deps master' imports', text');
   50.40 +        val current =
   50.41 +          #2 master = #2 master' andalso
   50.42 +            (case lookup_theory name of
   50.43 +              NONE => false
   50.44 +            | SOME theory => Thy_Load.all_current theory);
   50.45 +      in (current, deps', imports') end);
   50.46  
   50.47  in
   50.48  
   50.49 @@ -285,14 +281,15 @@
   50.50        SOME task => (task_finished task, tasks)
   50.51      | NONE =>
   50.52          let
   50.53 -          val (current, deps, imports, opt_text) = check_deps dir' name
   50.54 +          val (current, deps, imports) = check_deps dir' name
   50.55              handle ERROR msg => cat_error msg
   50.56                (loader_msg "the error(s) above occurred while examining theory" [name] ^
   50.57                  required_by "\n" initiators);
   50.58  
   50.59            val parents = map base_name imports;
   50.60            val (parents_current, tasks') =
   50.61 -            require_thys (name :: initiators) (Path.append dir (master_dir deps)) imports tasks;
   50.62 +            require_thys (name :: initiators)
   50.63 +              (Path.append dir (master_dir (Option.map #1 deps))) imports tasks;
   50.64  
   50.65            val all_current = current andalso parents_current;
   50.66            val task =
   50.67 @@ -300,10 +297,8 @@
   50.68              else
   50.69                (case deps of
   50.70                  NONE => raise Fail "Malformed deps"
   50.71 -              | SOME (dep as {master = (thy_path, _), ...}) =>
   50.72 -                  let
   50.73 -                    val text = (case opt_text of SOME text => text | NONE => File.read thy_path);
   50.74 -                    val update_time = serial ();
   50.75 +              | SOME (dep, text) =>
   50.76 +                  let val update_time = serial ()
   50.77                    in Task (parents, load_thy initiators update_time dep text name) end);
   50.78          in (all_current, new_entry name parents task tasks') end)
   50.79    end;
   50.80 @@ -336,7 +331,7 @@
   50.81  fun register_thy theory =
   50.82    let
   50.83      val name = Context.theory_name theory;
   50.84 -    val master = Thy_Load.check_thy (Thy_Load.master_directory theory) name;
   50.85 +    val {master, ...} = Thy_Load.check_thy (Thy_Load.master_directory theory) name;
   50.86      val parents = map Context.theory_name (Theory.parents_of theory);
   50.87      val imports = Thy_Load.imports_of theory;
   50.88      val deps = make_deps master imports;
    51.1 --- a/src/Pure/Thy/thy_load.ML	Fri Mar 18 18:19:42 2011 +0100
    51.2 +++ b/src/Pure/Thy/thy_load.ML	Mon Mar 21 08:29:16 2011 +0100
    51.3 @@ -1,27 +1,25 @@
    51.4  (*  Title:      Pure/Thy/thy_load.ML
    51.5 -    Author:     Markus Wenzel, TU Muenchen
    51.6 +    Author:     Makarius
    51.7  
    51.8 -Loading files that contribute to a theory, including global load path
    51.9 -management.
   51.10 +Loading files that contribute to a theory.  Global master path.
   51.11  *)
   51.12  
   51.13  signature THY_LOAD =
   51.14  sig
   51.15 -  val set_master_path: Path.T -> unit
   51.16 -  val get_master_path: unit -> Path.T
   51.17    val master_directory: theory -> Path.T
   51.18    val imports_of: theory -> string list
   51.19    val provide: Path.T * (Path.T * SHA1.digest) -> theory -> theory
   51.20 -  val check_file: Path.T -> Path.T -> Path.T * SHA1.digest
   51.21 -  val check_thy: Path.T -> string -> Path.T * SHA1.digest
   51.22 -  val deps_thy: Path.T -> string ->
   51.23 -   {master: Path.T * SHA1.digest, text: string, imports: string list, uses: Path.T list}
   51.24 +  val check_file: Path.T -> Path.T -> Path.T
   51.25 +  val check_thy: Path.T -> string ->
   51.26 +    {master: Path.T * SHA1.digest, text: string, imports: string list, uses: (Path.T * bool) list}
   51.27    val loaded_files: theory -> Path.T list
   51.28    val all_current: theory -> bool
   51.29    val provide_file: Path.T -> theory -> theory
   51.30    val use_ml: Path.T -> unit
   51.31    val exec_ml: Path.T -> generic_theory -> generic_theory
   51.32    val begin_theory: Path.T -> string -> string list -> theory list -> (Path.T * bool) list -> theory
   51.33 +  val set_master_path: Path.T -> unit
   51.34 +  val get_master_path: unit -> Path.T
   51.35  end;
   51.36  
   51.37  structure Thy_Load: THY_LOAD =
   51.38 @@ -69,51 +67,25 @@
   51.39      else (master_dir, imports, required, (src_path, path_id) :: provided));
   51.40  
   51.41  
   51.42 -(* stateful master path *)
   51.43 -
   51.44 -local
   51.45 -  val master_path = Unsynchronized.ref Path.current;
   51.46 -in
   51.47 -
   51.48 -fun set_master_path path = master_path := path;
   51.49 -fun get_master_path () = ! master_path;
   51.50 -
   51.51 -end;
   51.52 -
   51.53 -
   51.54  (* check files *)
   51.55  
   51.56 -fun get_file dir src_path =
   51.57 +fun check_file dir file = File.check_file (File.full_path dir file);
   51.58 +
   51.59 +fun digest_file dir file =
   51.60    let
   51.61 -    val path = Path.expand src_path;
   51.62 -    val _ = Path.is_current path andalso error "Bad file specification";
   51.63 -    val full_path = File.full_path (Path.append dir path);
   51.64 -  in
   51.65 -    if File.exists full_path
   51.66 -    then SOME (full_path, SHA1.digest (File.read full_path))
   51.67 -    else NONE
   51.68 -  end;
   51.69 -
   51.70 -fun check_file dir file =
   51.71 -  (case get_file dir file of
   51.72 -    SOME path_id => path_id
   51.73 -  | NONE => error ("Could not find file " ^ Path.print file ^ "\nin " ^ Path.print dir));
   51.74 +    val full_path = check_file dir file;
   51.75 +    val id = SHA1.digest (File.read full_path);
   51.76 +  in (full_path, id) end;
   51.77  
   51.78  fun check_thy dir name =
   51.79 -  check_file dir (Thy_Header.thy_path name);
   51.80 -
   51.81 -
   51.82 -(* theory deps *)
   51.83 -
   51.84 -fun deps_thy master_dir name =
   51.85    let
   51.86 -    val master as (thy_path, _) = check_thy master_dir name;
   51.87 -    val text = File.read thy_path;
   51.88 -    val (name', imports, uses) = Thy_Header.read (Path.position thy_path) text;
   51.89 +    val master_file = check_file dir (Thy_Header.thy_path name);
   51.90 +    val text = File.read master_file;
   51.91 +    val (name', imports, uses) =
   51.92 +      if name = Context.PureN then (Context.PureN, [], [])
   51.93 +      else Thy_Header.read (Path.position master_file) text;
   51.94      val _ = Thy_Header.consistent_name name name';
   51.95 -    val uses = map (Path.explode o #1) uses;
   51.96 -  in {master = master, text = text, imports = imports, uses = uses} end;
   51.97 -
   51.98 +  in {master = (master_file, SHA1.digest text), text = text, imports = imports, uses = uses} end;
   51.99  
  51.100  
  51.101  (* loaded files *)
  51.102 @@ -138,7 +110,7 @@
  51.103    let
  51.104      val {master_dir, provided, ...} = Files.get thy;
  51.105      fun current (src_path, (_, id)) =
  51.106 -      (case get_file master_dir src_path of
  51.107 +      (case try (digest_file master_dir) src_path of
  51.108          NONE => false
  51.109        | SOME (_, id') => id = id');
  51.110    in can check_loaded thy andalso forall current provided end;
  51.111 @@ -149,15 +121,15 @@
  51.112  (* provide files *)
  51.113  
  51.114  fun provide_file src_path thy =
  51.115 -  provide (src_path, check_file (master_directory thy) src_path) thy;
  51.116 +  provide (src_path, digest_file (master_directory thy) src_path) thy;
  51.117  
  51.118  fun use_ml src_path =
  51.119    if is_none (Context.thread_data ()) then
  51.120 -    ML_Context.eval_file (#1 (check_file Path.current src_path))
  51.121 +    ML_Context.eval_file (check_file Path.current src_path)
  51.122    else
  51.123      let
  51.124        val thy = ML_Context.the_global_context ();
  51.125 -      val (path, id) = check_file (master_directory thy) src_path;
  51.126 +      val (path, id) = digest_file (master_directory thy) src_path;
  51.127  
  51.128        val _ = ML_Context.eval_file path;
  51.129        val _ = Context.>> Local_Theory.propagate_ml_env;
  51.130 @@ -178,5 +150,16 @@
  51.131    |> fold (fn (path, true) => Context.theory_map (exec_ml path) o Theory.checkpoint | _ => I) uses
  51.132    |> Theory.checkpoint;
  51.133  
  51.134 +
  51.135 +(* global master path *)
  51.136 +
  51.137 +local
  51.138 +  val master_path = Unsynchronized.ref Path.current;
  51.139 +in
  51.140 +
  51.141 +fun set_master_path path = master_path := path;
  51.142 +fun get_master_path () = ! master_path;
  51.143 +
  51.144  end;
  51.145  
  51.146 +end;
    52.1 --- a/src/Pure/Tools/find_consts.ML	Fri Mar 18 18:19:42 2011 +0100
    52.2 +++ b/src/Pure/Tools/find_consts.ML	Mon Mar 21 08:29:16 2011 +0100
    52.3 @@ -69,7 +69,7 @@
    52.4  
    52.5  fun find_consts ctxt raw_criteria =
    52.6    let
    52.7 -    val start = start_timing ();
    52.8 +    val start = Timing.start ();
    52.9  
   52.10      val thy = ProofContext.theory_of ctxt;
   52.11      val low_ranking = 10000;
   52.12 @@ -114,7 +114,7 @@
   52.13        |> sort (rev_order o int_ord o pairself snd)
   52.14        |> map (apsnd fst o fst);
   52.15  
   52.16 -    val end_msg = " in " ^ Time.toString (#cpu (end_timing start)) ^ " secs";
   52.17 +    val end_msg = " in " ^ Time.toString (#cpu (Timing.result start)) ^ " secs";
   52.18    in
   52.19      Pretty.big_list "searched for:" (map pretty_criterion raw_criteria) ::
   52.20      Pretty.str "" ::
    53.1 --- a/src/Pure/Tools/find_theorems.ML	Fri Mar 18 18:19:42 2011 +0100
    53.2 +++ b/src/Pure/Tools/find_theorems.ML	Mon Mar 21 08:29:16 2011 +0100
    53.3 @@ -464,7 +464,7 @@
    53.4  
    53.5  fun print_theorems ctxt opt_goal opt_limit rem_dups raw_criteria =
    53.6    let
    53.7 -    val start = start_timing ();
    53.8 +    val start = Timing.start ();
    53.9  
   53.10      val criteria = map (apsnd (read_criterion ctxt)) raw_criteria;
   53.11      val (foundo, theorems) = filter_theorems ctxt (map Internal (all_facts_of ctxt))
   53.12 @@ -480,7 +480,7 @@
   53.13               then " (" ^ string_of_int returned ^ " displayed)"
   53.14               else ""));
   53.15  
   53.16 -    val end_msg = " in " ^ Time.toString (#cpu (end_timing start)) ^ " secs";
   53.17 +    val end_msg = " in " ^ Time.toString (#cpu (Timing.result start)) ^ " secs";
   53.18    in
   53.19      Pretty.big_list "searched for:" (map (pretty_criterion ctxt) criteria) ::
   53.20      Pretty.str "" ::
    54.1 --- a/src/Pure/theory.ML	Fri Mar 18 18:19:42 2011 +0100
    54.2 +++ b/src/Pure/theory.ML	Mon Mar 21 08:29:16 2011 +0100
    54.3 @@ -84,7 +84,7 @@
    54.4  
    54.5  fun make_thy (axioms, defs, wrappers) = Thy {axioms = axioms, defs = defs, wrappers = wrappers};
    54.6  
    54.7 -structure ThyData = Theory_Data_PP
    54.8 +structure Thy = Theory_Data_PP
    54.9  (
   54.10    type T = thy;
   54.11    val empty_axioms = Name_Space.empty_table "axiom" : term Name_Space.table;
   54.12 @@ -104,9 +104,9 @@
   54.13      in make_thy (axioms', defs', (bgs', ens')) end;
   54.14  );
   54.15  
   54.16 -fun rep_theory thy = ThyData.get thy |> (fn Thy args => args);
   54.17 +fun rep_theory thy = Thy.get thy |> (fn Thy args => args);
   54.18  
   54.19 -fun map_thy f = ThyData.map (fn (Thy {axioms, defs, wrappers}) =>
   54.20 +fun map_thy f = Thy.map (fn (Thy {axioms, defs, wrappers}) =>
   54.21    make_thy (f (axioms, defs, wrappers)));
   54.22  
   54.23  
    55.1 --- a/src/Tools/Code/code_haskell.ML	Fri Mar 18 18:19:42 2011 +0100
    55.2 +++ b/src/Tools/Code/code_haskell.ML	Mon Mar 21 08:29:16 2011 +0100
    55.3 @@ -350,7 +350,7 @@
    55.4      (*serialization*)
    55.5      fun write_module width (SOME destination) (module_name, content) =
    55.6            let
    55.7 -            val _ = File.check destination;
    55.8 +            val _ = File.check_dir destination;
    55.9              val filepath = (Path.append destination o Path.ext "hs" o Path.explode o implode
   55.10                o separate "/" o Long_Name.explode) module_name;
   55.11              val _ = Isabelle_System.mkdirs (Path.dir filepath);
    56.1 --- a/src/Tools/quickcheck.ML	Fri Mar 18 18:19:42 2011 +0100
    56.2 +++ b/src/Tools/quickcheck.ML	Mon Mar 21 08:29:16 2011 +0100
    56.3 @@ -166,12 +166,9 @@
    56.4        error "Term to be tested contains schematic variables";
    56.5    in () end
    56.6  
    56.7 -fun cpu_time description f =
    56.8 -  let
    56.9 -    val start = start_timing ()
   56.10 -    val result = Exn.capture f ()
   56.11 -    val time = Time.toMilliseconds (#cpu (end_timing start))
   56.12 -  in (Exn.release result, (description, time)) end
   56.13 +fun cpu_time description e =
   56.14 +  let val ({cpu, ...}, result) = Timing.timing e ()
   56.15 +  in (result, (description, Time.toMilliseconds cpu)) end
   56.16  
   56.17  fun limit ctxt (limit_time, is_interactive) f exc () =
   56.18    if limit_time then