--- a/Admin/isatest/settings/at-mac-poly-5.1-para Tue Jul 21 07:54:44 2009 +0200
+++ b/Admin/isatest/settings/at-mac-poly-5.1-para Tue Jul 21 07:55:56 2009 +0200
@@ -25,4 +25,4 @@
ISABELLE_USEDIR_OPTIONS="-i false -d false -M 4"
-HOL_USEDIR_OPTIONS="-p 2 -Q false"
+HOL_USEDIR_OPTIONS="-p 2 -q 0"
--- a/Admin/isatest/settings/at-poly-5.1-para-e Tue Jul 21 07:54:44 2009 +0200
+++ b/Admin/isatest/settings/at-poly-5.1-para-e Tue Jul 21 07:55:56 2009 +0200
@@ -24,4 +24,4 @@
ISABELLE_USEDIR_OPTIONS="-i true -d pdf -v true -M 20"
-HOL_USEDIR_OPTIONS="-p 2 -Q false"
+HOL_USEDIR_OPTIONS="-p 2 -q 0"
--- a/Admin/isatest/settings/at64-poly-5.1-para Tue Jul 21 07:54:44 2009 +0200
+++ b/Admin/isatest/settings/at64-poly-5.1-para Tue Jul 21 07:55:56 2009 +0200
@@ -24,4 +24,4 @@
ISABELLE_USEDIR_OPTIONS="-i true -d pdf -v true -M 2"
-HOL_USEDIR_OPTIONS="-p 2 -Q false"
+HOL_USEDIR_OPTIONS="-p 2 -q 0"
--- a/Admin/isatest/settings/mac-poly-M4 Tue Jul 21 07:54:44 2009 +0200
+++ b/Admin/isatest/settings/mac-poly-M4 Tue Jul 21 07:55:56 2009 +0200
@@ -25,4 +25,4 @@
ISABELLE_USEDIR_OPTIONS="-i false -d false -M 4"
-HOL_USEDIR_OPTIONS="-p 2 -Q false"
+HOL_USEDIR_OPTIONS="-p 2 -q 1"
--- a/Admin/isatest/settings/mac-poly-M8 Tue Jul 21 07:54:44 2009 +0200
+++ b/Admin/isatest/settings/mac-poly-M8 Tue Jul 21 07:55:56 2009 +0200
@@ -25,4 +25,4 @@
ISABELLE_USEDIR_OPTIONS="-i false -d false -M 8"
-HOL_USEDIR_OPTIONS="-p 2 -Q false"
+HOL_USEDIR_OPTIONS="-p 2 -q 1"
--- a/Admin/isatest/settings/mac-poly64-M4 Tue Jul 21 07:54:44 2009 +0200
+++ b/Admin/isatest/settings/mac-poly64-M4 Tue Jul 21 07:55:56 2009 +0200
@@ -25,4 +25,4 @@
ISABELLE_USEDIR_OPTIONS="-i false -d false -M 4"
-HOL_USEDIR_OPTIONS="-p 2 -Q false"
+HOL_USEDIR_OPTIONS="-p 2 -q 1"
--- a/doc-src/IsarRef/showsymbols Tue Jul 21 07:54:44 2009 +0200
+++ b/doc-src/IsarRef/showsymbols Tue Jul 21 07:55:56 2009 +0200
@@ -1,6 +1,4 @@
#!/usr/bin/env perl
-#
-# $Id$
print "\\begin{supertabular}{ll\@{\\qquad}ll}\n";
--- a/doc-src/System/Makefile Tue Jul 21 07:54:44 2009 +0200
+++ b/doc-src/System/Makefile Tue Jul 21 07:55:56 2009 +0200
@@ -1,7 +1,3 @@
-#
-# $Id$
-#
-
## targets
default: dvi
--- a/doc-src/System/Thy/Basics.thy Tue Jul 21 07:54:44 2009 +0200
+++ b/doc-src/System/Thy/Basics.thy Tue Jul 21 07:55:56 2009 +0200
@@ -1,5 +1,3 @@
-(* $Id$ *)
-
theory Basics
imports Pure
begin
--- a/doc-src/System/Thy/Interfaces.thy Tue Jul 21 07:54:44 2009 +0200
+++ b/doc-src/System/Thy/Interfaces.thy Tue Jul 21 07:55:56 2009 +0200
@@ -1,5 +1,3 @@
-(* $Id$ *)
-
theory Interfaces
imports Pure
begin
--- a/doc-src/System/Thy/Misc.thy Tue Jul 21 07:54:44 2009 +0200
+++ b/doc-src/System/Thy/Misc.thy Tue Jul 21 07:55:56 2009 +0200
@@ -1,5 +1,3 @@
-(* $Id$ *)
-
theory Misc
imports Pure
begin
--- a/doc-src/System/Thy/Presentation.thy Tue Jul 21 07:54:44 2009 +0200
+++ b/doc-src/System/Thy/Presentation.thy Tue Jul 21 07:55:56 2009 +0200
@@ -1,5 +1,3 @@
-(* $Id$ *)
-
theory Presentation
imports Pure
begin
@@ -442,7 +440,6 @@
-D PATH dump generated document sources into PATH
-M MAX multithreading: maximum number of worker threads (default 1)
-P PATH set path for remote theory browsing information
- -Q BOOL check proofs in parallel (default true)
-T LEVEL multithreading: trace level (default 0)
-V VERSION declare alternative document VERSION
-b build mode (output heap image, using current dir)
--- a/doc-src/System/Thy/ROOT.ML Tue Jul 21 07:54:44 2009 +0200
+++ b/doc-src/System/Thy/ROOT.ML Tue Jul 21 07:55:56 2009 +0200
@@ -1,6 +1,3 @@
-
-(* $Id$ *)
-
set ThyOutput.source;
use "../../antiquote_setup.ML";
--- a/doc-src/System/Thy/document/Basics.tex Tue Jul 21 07:54:44 2009 +0200
+++ b/doc-src/System/Thy/document/Basics.tex Tue Jul 21 07:55:56 2009 +0200
@@ -3,8 +3,6 @@
\def\isabellecontext{Basics}%
%
\isadelimtheory
-\isanewline
-\isanewline
%
\endisadelimtheory
%
--- a/doc-src/System/Thy/document/Interfaces.tex Tue Jul 21 07:54:44 2009 +0200
+++ b/doc-src/System/Thy/document/Interfaces.tex Tue Jul 21 07:55:56 2009 +0200
@@ -3,8 +3,6 @@
\def\isabellecontext{Interfaces}%
%
\isadelimtheory
-\isanewline
-\isanewline
%
\endisadelimtheory
%
--- a/doc-src/System/Thy/document/Misc.tex Tue Jul 21 07:54:44 2009 +0200
+++ b/doc-src/System/Thy/document/Misc.tex Tue Jul 21 07:55:56 2009 +0200
@@ -3,8 +3,6 @@
\def\isabellecontext{Misc}%
%
\isadelimtheory
-\isanewline
-\isanewline
%
\endisadelimtheory
%
--- a/doc-src/System/Thy/document/Presentation.tex Tue Jul 21 07:54:44 2009 +0200
+++ b/doc-src/System/Thy/document/Presentation.tex Tue Jul 21 07:55:56 2009 +0200
@@ -3,8 +3,6 @@
\def\isabellecontext{Presentation}%
%
\isadelimtheory
-\isanewline
-\isanewline
%
\endisadelimtheory
%
@@ -468,7 +466,6 @@
-D PATH dump generated document sources into PATH
-M MAX multithreading: maximum number of worker threads (default 1)
-P PATH set path for remote theory browsing information
- -Q BOOL check proofs in parallel (default true)
-T LEVEL multithreading: trace level (default 0)
-V VERSION declare alternative document VERSION
-b build mode (output heap image, using current dir)
--- a/doc-src/System/system.tex Tue Jul 21 07:54:44 2009 +0200
+++ b/doc-src/System/system.tex Tue Jul 21 07:55:56 2009 +0200
@@ -1,6 +1,3 @@
-
-%% $Id$
-
\documentclass[12pt,a4paper]{report}
\usepackage{supertabular}
\usepackage{graphicx}
--- a/src/Pure/codegen.ML Tue Jul 21 07:54:44 2009 +0200
+++ b/src/Pure/codegen.ML Tue Jul 21 07:55:56 2009 +0200
@@ -64,7 +64,7 @@
val new_name: term -> string -> string
val if_library: 'a -> 'a -> 'a
val get_defn: theory -> deftab -> string -> typ ->
- ((typ * (string * (term list * term))) * int option) option
+ ((typ * (string * thm)) * int option) option
val is_instance: typ -> typ -> bool
val parens: Pretty.T -> Pretty.T
val mk_app: bool -> Pretty.T -> Pretty.T list -> Pretty.T
@@ -147,8 +147,7 @@
type deftab =
(typ * (* type of constant *)
(string * (* name of theory containing definition of constant *)
- (term list * (* parameters *)
- term))) (* right-hand side *)
+ thm)) (* definition theorem *)
list Symtab.table;
(* code dependency graph *)
@@ -490,35 +489,43 @@
fun get_aux_code xs = map_filter (fn (m, code) =>
if m = "" orelse member (op =) (!mode) m then SOME code else NONE) xs;
+fun dest_prim_def t =
+ let
+ val (lhs, rhs) = Logic.dest_equals t;
+ val (c, args) = strip_comb lhs;
+ val (s, T) = dest_Const c
+ in if forall is_Var args then SOME (s, (T, (args, rhs))) else NONE
+ end handle TERM _ => NONE;
+
fun mk_deftab thy =
let
val axmss = map (fn thy' => (Context.theory_name thy', Theory.axiom_table thy'))
(thy :: Theory.ancestors_of thy);
fun prep_def def = (case preprocess thy [def] of
[def'] => prop_of def' | _ => error "mk_deftab: bad preprocessor");
- fun dest t =
- let
- val (lhs, rhs) = Logic.dest_equals t;
- val (c, args) = strip_comb lhs;
- val (s, T) = dest_Const c
- in if forall is_Var args then SOME (s, (T, (args, rhs))) else NONE
- end handle TERM _ => NONE;
- fun add_def thyname (name, t) = (case dest t of
+ fun add_def thyname (name, t) = (case dest_prim_def t of
NONE => I
- | SOME _ => (case dest (prep_def (Thm.axiom thy name)) of
- NONE => I
- | SOME (s, (T, (args, rhs))) => Symtab.map_default (s, [])
- (cons (T, (thyname, split_last (rename_terms (args @ [rhs])))))))
+ | SOME (s, (T, _)) => Symtab.map_default (s, [])
+ (cons (T, (thyname, Thm.axiom thy name))));
in
fold (fn (thyname, axms) => Symtab.fold (add_def thyname) axms) axmss Symtab.empty
end;
+fun prep_prim_def thy thm =
+ let
+ val prop = case preprocess thy [thm]
+ of [thm'] => Thm.prop_of thm'
+ | _ => error "mk_deftab: bad preprocessor"
+ in ((Option.map o apsnd o apsnd)
+ (fn (args, rhs) => split_last (rename_terms (args @ [rhs]))) o dest_prim_def) prop
+ end;
+
fun get_defn thy defs s T = (case Symtab.lookup defs s of
NONE => NONE
| SOME ds =>
let val i = find_index (is_instance T o fst) ds
in if i >= 0 then
- SOME (List.nth (ds, i), if length ds = 1 then NONE else SOME i)
+ SOME (nth ds i, if length ds = 1 then NONE else SOME i)
else NONE
end);
@@ -655,8 +662,8 @@
end
| NONE => (case get_defn thy defs s T of
NONE => NONE
- | SOME ((U, (thyname, (args, rhs))), k) =>
- let
+ | SOME ((U, (thyname, thm)), k) => (case prep_prim_def thy thm
+ of SOME (_, (_, (args, rhs))) => let
val module' = if_library thyname module;
val suffix = (case k of NONE => "" | SOME i => " def" ^ string_of_int i);
val node_id = s ^ suffix;
@@ -686,7 +693,8 @@
[str " =", Pretty.brk 1, p', str ";"])) ^ "\n\n")) gr4)
end
| SOME _ => (p, add_edge (node_id, dep) gr'))
- end))
+ end
+ | NONE => NONE)))
| Abs _ =>
let