src/Pure/ProofGeneral/pgip.ML
author wenzelm
Fri, 18 Jan 2013 16:20:09 +0100
changeset 50974 55f8bd61b029
parent 29606 fedb8be05f24
permissions -rw-r--r--
added "tasks_proof" statistics, via slighly odd global reference Future.forked_proofs (NB: Future.report_status is intertwined with scheduler thread);
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
21637
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
     1
(*  Title:      Pure/ProofGeneral/pgip.ML
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
     2
    Author:     David Aspinall
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
     3
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
     4
Prover-side PGIP abstraction.  
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
     5
Not too closely tied to Isabelle, to help with reuse/porting.
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
     6
*)
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
     7
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
     8
signature PGIP =
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
     9
sig
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
    10
    include PGIPTYPES
21641
d73ab30e82dc Include pgip markup module
aspinall
parents: 21637
diff changeset
    11
    include PGIPMARKUP
21637
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
    12
    include PGIPINPUT
21641
d73ab30e82dc Include pgip markup module
aspinall
parents: 21637
diff changeset
    13
    include PGIPOUTPUT
21637
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
    14
end
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
    15
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
    16
structure Pgip : PGIP = 
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
    17
struct
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
    18
   open PgipTypes
21641
d73ab30e82dc Include pgip markup module
aspinall
parents: 21637
diff changeset
    19
   open PgipMarkup
21637
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
    20
   open PgipInput
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
    21
   open PgipOutput
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
    22
end