c# pdf to image free library : Convert pdf fillable form to html application control tool html web page winforms online system2-part857

CHAPTER 2. ISABELLE SESSIONS AND BUILD MANAGEMENT
18
Isabelle sessions are defined via session ROOT files as described in (§2.1).
The totality of sessions is determined by collecting such specifications from
all Isabelle component directories (§1.1.3), augmented by more directories
given via options -d DIR on the command line. Each such directory may
contain a session ROOT file with several session specifications.
Any session root directory may refer recursively to further directories of the
same kind, by listing them in a catalog file ROOTS line-by-line. This helps to
organize large collections of session specifications, or to make -d command
line options persistent (say within $ISABELLE_HOME_USER/ROOTS).
The subset of sessions to be managed is determined via individual SESSIONS
given as command-line arguments, or session groups that are given via one or
more options -g NAME. Option -a selects all sessions. The build tool takes
session dependencies into account: the set of selected sessions is completed
by including all ancestors.
One or more options -x NAME specify sessions to be excluded. All descen-
dents of excluded sessions are removed from the selection as specified above.
Option -X is analogous to this, but excluded sessions are specified by session
group membership.
Option -R reverses the selection in the sense that it refers to its requirements:
all ancestor sessions excluding the original selection. This allows to prepare
the stage for some build process with different options, before running the
main build itself (without option -R).
Option -D is similar to -d, but selects all sessions that are defined in the
given directories.
The build process depends on additional options (§2.2) that are passed to the
prover eventually. The settings variable ISABELLE_BUILD_OPTIONS allows to
provide additional defaults, e.g. ISABELLE_BUILD_OPTIONS="document=pdf
threads=4". Moreover, the environment of system build options may be
augmented on the command line via -o name=value or -o name, which ab-
breviates -o name=true for Boolean options. Multiple occurrences of -o on
the command-line are applied in the given order.
Option -b ensures that heap images are produced for all selected sessions.
By default, images are only saved for inner nodes of the hierarchy of sessions,
as required for other sessions to continue later on.
Option -c cleans all descendants of the selected sessions before performing
the specified build operation.
Convert pdf fillable form to html - C# PDF Form Data fill-in Library: auto fill-in PDF form data in C#.net, ASP.NET, MVC, WinForms, WPF
Online C# Tutorial to Automatically Fill in Field Data to PDF
convert word form to fillable pdf form; best pdf form filler
Convert pdf fillable form to html - VB.NET PDF Form Data fill-in library: auto fill-in PDF form data in vb.net, ASP.NET, MVC, WinForms, WPF
VB.NET PDF Form Data fill-in library: auto fill-in PDF form data in vb.net, ASP.NET, MVC, WinForms, WPF
asp.net fill pdf form; convert excel to fillable pdf form
CHAPTER 2. ISABELLE SESSIONS AND BUILD MANAGEMENT
19
Option -n omits the actual build process after the preparatory stage (includ-
ing optional cleanup). Note that the return code always indicates the status
of the set of selected sessions.
Option -j specifies the maximum number of parallel build jobs (prover pro-
cesses). Each prover process is subject to a separate limit of parallel worker
threads, cf. system option threads.
Option -s enables system mode, which means that resulting heap images and
log files are stored in $ISABELLE_HOME/heaps instead of the default location
ISABELLE_OUTPUT (which is normally in ISABELLE_HOME_USER, i.e. the user’s
home directory).
Option -v increases the general level of verbosity. Option -l lists the source
files that contribute to a session.
Option -k specifies a newly proposed keyword for outer syntax (multiple uses
allowed). The theory sources are checked for conflicts wrt. this hypothetical
change of syntax, e.g. to reveal occurrences of identifiers that need to be
quoted.
Examples
Build a specific logic image:
isabelle build -b HOLCF
Build the main group of logic images:
isabelle build -b -g main
Provide a general overview of the status of all Isabelle sessions, without
building anything:
isabelle build -a -n -v
Build all sessions with HTML browser info and PDF document preparation:
isabelle build -a -o browser_info -o document=pdf
Build all sessions with a maximum of8 parallel prover processes and 4worker
threads each (on a machine with many cores):
isabelle build -a -j8 -o threads=4
VB.NET Create PDF from PowerPoint Library to convert pptx, ppt to
Convert to PDF with embedded fonts or without original fonts fast. Convert multiple pages PowerPoint to fillable and editable PDF documents.
convert html form to pdf fillable form; change font size pdf fillable form
VB.NET Create PDF from Excel Library to convert xlsx, xls to PDF
Create fillable and editable PDF documents from Excel in Create searchable and scanned PDF files from Excel in VB Convert to PDF with embedded fonts or without
change font pdf fillable form; change font size in pdf fillable form
CHAPTER 2. ISABELLE SESSIONS AND BUILD MANAGEMENT
20
Build some session images with cleanup of their descendants, while retaining
their ancestry:
isabelle build -b -c HOL-Algebra HOL-Word
Clean all sessions without building anything:
isabelle build -a -n -c
Build all sessions from some other directory hierarchy, according to the set-
tings variable AFP that happens to be defined inside the Isabelle environment:
isabelle build -D ’$AFP’
Inform about the status of all sessions required for AFP, without building
anything yet:
isabelle build -D ’$AFP’ -R -v -n
VB.NET Create PDF from Word Library to convert docx, doc to PDF in
Create PDF files from both DOC and DOCX formats. Convert multiple pages Word to fillable and editable PDF documents.
convert pdf into fillable form; adding a signature to a pdf form
C# Create PDF from OpenOffice to convert odt, odp files to PDF in
Convert OpenOffice Text Document to PDF with embedded Create PDF document from OpenOffice Presentation in both ODT, ODS, ODP forms to fillable PDF formats in
create fillable forms in pdf; .net fill pdf form
Chapter 3
Presenting theories
Isabelle provides several waysto present theoutcomeof formal developments,
including WWW-based browsable libraries or actual printable documents.
Presentation is centered around the concept of sessions (chapter 2). The
global session structure is that of a tree, with Isabelle Pure at its root, further
object-logics derived (e.g. HOLCF from HOL, and HOL from Pure), and
application sessions further on in the hierarchy.
The tools isabelle mkroot and isabelle build provide the primary
meansfor managingIsabelle sessions, includingproper setup for presentation;
isabelle build takes care to have isabelle_process run any additional
stages required for document preparation, notably the isabelle document
and isabelle latex. The complete tool chain for managing batch-mode
Isabelle sessions is illustrated in figure 3.1.
isabelle mkroot
invoked once by the user to initialize the ses-
sion ROOT with optional document directory;
isabelle build
invoked repeatedly by the user to keep session
output up-to-date (HTML, documents etc.);
isabelle_process
run through isabelle build;
isabelle document run by the Isabelle process if document prepa-
ration is enabled;
isabelle latex
universal L
A
T
E
Xtool wrapper invoked multiple
times by isabelle document; also useful for
manual experiments;
Figure 3.1: The tool chain of Isabelle session presentation
3.1 Generating HTML browser information
As a side-effect of building sessions, Isabelle is able to generate theory brows-
ing information, including HTML documents that show the theory sources
21
C# PDF Field Edit Library: insert, delete, update pdf form field
A professional PDF form creator supports to create fillable PDF form in C#.NET. An advanced PDF form maker allows users to create editable PDF form in C#.NET.
create fillable form from pdf; allow users to attach to pdf form
C# Create PDF from Excel Library to convert xlsx, xls to PDF in C#
Create fillable and editable PDF documents from Excel in both .NET WinForms and ASP.NET. Create searchable and scanned PDF files from Excel. Convert to PDF with
adding signature to pdf form; create fill pdf form
CHAPTER 3. PRESENTING THEORIES
22
and the relationship with its ancestors and descendants. Besides the HTML
file that is generated for every theory, Isabelle stores links to all theories
of a session in an index file. As a second hierarchy, groups of sessions are
organized as chapters, with a separate index. Note that the implicit tree
structure of the session build hierarchy is not relevant for the presentation.
To generate theory browsing information for an existing session, just invoke
isabelle build with suitable options:
isabelle build -o browser_info -v -c FOL
The presentation output will appear in $ISABELLE_BROWSER_INFO/FOL/FOL
as reported by the above verbose invocation of the build process.
Many Isabelle sessions (such as HOL-Library in ~~/src/HOL/Library) also
provide printable documents in PDF. These are prepared automatically as
well if enabled like this:
isabelle build -o browser_info -o document=pdf -v -c HOL-Library
Enabling both browser info and document preparation simultaneously causes
an appropriate “document” link to be included in the HTML index. Docu-
ments may be generated independently of browser information as well, see
§3.3 for further details.
The theory browsing information is stored in a sub-directory directory deter-
mined by the ISABELLE_BROWSER_INFO setting plus a prefix corresponding
to the session chapter and identifier. In order to present Isabelle applications
on the web, the corresponding subdirectory from ISABELLE_BROWSER_INFO
can be put on a WWW server.
3.2 Preparing session root directories
The isabelle mkroot tool configures a given directory as session root, with
some ROOT file and optional document source directory. Its usage is:
Usage: isabelle mkroot [OPTIONS] [DIR]
Options are:
-d
enable document preparation
-n NAME
alternative session name (default: DIR base name)
Prepare session root DIR (default: current directory).
C# Create PDF from PowerPoint Library to convert pptx, ppt to PDF
Convert multiple pages PowerPoint to fillable and editable PDF documents. Easy to create searchable and scanned PDF files from PowerPoint.
convert word to pdf fillable form; create a pdf form that can be filled out
C# Create PDF from Word Library to convert docx, doc to PDF in C#.
Convert multiple pages Word to fillable and editable PDF documents in both .NET WinForms and ASP.NET. Convert both DOC and DOCX formats to PDF files.
convert pdf fillable form to html; convert pdf file to fillable form
CHAPTER 3. PRESENTING THEORIES
23
The results are placed in the given directory dir, which refers to the current
directory by default. The isabelle mkroot tool is conservative in the sense
that it does not overwrite existing files or directories. Earlier attempts to
generate a session root need to be deleted manually.
Option -d indicates that the session shall be accompanied by a formal doc-
ument, with DIR/document/root.tex as its L
A
T
E
X entry point (see also
chapter 3).
Option -n allows to specify an alternative session name; otherwise the base
name of the given directory is used.
The implicit Isabelle settings variable ISABELLE_LOGIC specifies the parent
session, and ISABELLE_DOCUMENT_FORMAT the document format to be filled
filled into the generated ROOT file.
Examples
Produce session Test (with document preparation) within a separate direc-
tory of the same name:
isabelle mkroot -d Test && isabelle build -D Test
Upgrade the current directory into a session ROOT with document prepara-
tion, and build it:
isabelle mkroot -d && isabelle build -D .
3.3 Preparing Isabelle session documents
The isabelle document tool prepares logic session documents, processing
the sources as provided by the user and generated by Isabelle. Its usage is:
Usage: isabelle document [OPTIONS] [DIR]
Options are:
-c
cleanup -- be aggressive in removing old stuff
-n NAME
specify document name (default ’document’)
-o FORMAT
specify output format: pdf (default), dvi
-t TAGS
specify tagged region markup
Prepare the theory session document in DIR (default ’document’)
producing the specified output format.
C# Create PDF Library SDK to convert PDF from other file formats
Create writable PDF from text (.txt) file. HTML webpage to interactive PDF file creator freeware. Create fillable PDF document with fields.
convert pdf to pdf form fillable; change font in pdf fillable form
VB.NET Create PDF Library SDK to convert PDF from other file
Best VB.NET component to convert Microsoft Office Word Create and save editable PDF with a blank page Create fillable PDF document with fields in Visual Basic
convert pdf to fillable pdf form; pdf form filler
CHAPTER 3. PRESENTING THEORIES
24
This tool is usually run automatically as part of the Isabelle build process,
provided document preparation has been enabled via suitable options. It
may be manually invoked on the generated browser information document
output as well, e.g. in case of errors encountered in the batch run.
The -c option tells isabelle document to dispose the document sources
after successful operation! This is the right thing to do for sources gener-
ated by an Isabelle process, but take care of your files in manual document
preparation!
The -n and -o option specify the final output file name and format, the
default is “document.dvi”. Note that the result will appear in the parent of
the target DIR.
The -t option tells L
A
T
E
X how to interpret tagged Isabelle command re-
gions. Tags are specified as a comma separated list of modifier/name
pairs: “+foo” (or just “foo”) means to keep, “-foo” to drop, and “/foo”
to fold text tagged as foo. The builtin default is equivalent to the tag
specification “+theory,+proof,+ML,+visible,-invisible”; see also the
L
A
T
E
X macros \isakeeptag, \isadroptag, and \isafoldtag, in ~~/lib/
texinputs/isabelle.sty.
Document preparation requires a document directory within the session
sources. This directory is supposed to contain all the files needed to produce
the final document — apart from the actual theories which are generated by
Isabelle.
For most practical purposes, isabelle document is smart enough to create
any of the specified output formats, taking root.tex supplied by the user as
astarting point. This even includes multiple runs of L
A
T
E
Xto accommodate
references and bibliographies (the latter assumes root.bib within the same
directory).
In more complex situations, aseparate build script for the document sources
may be given. It is invoked with command-line arguments for the document
format and the document variant name. The script needs to produce cor-
responding output files, e.g. root.pdf for target format pdf (and default
variants). The main work can be again delegated to isabelle latex, but it
is also possible to harvest generated L
A
T
E
Xsources and copy them elsewhere.
When running the session, Isabelle copies the content of the original
document directory into its proper place within ISABELLE_BROWSER_INFO,
according to the session path and document variant. Then, for any processed
theory A some L
A
T
E
Xsource is generated and put there as A.tex. Further-
more, a list of all generated theory files is put into session.tex. Typically,
CHAPTER 3. PRESENTING THEORIES
25
the root L
A
T
E
Xfile provided by the user would include session.tex to get a
document containing all the theories.
The L
A
T
E
Xversions of the theories require some macros defined in ~~/lib/
texinputs/isabelle.sty. Doing \usepackage{isabelle} in root.tex
should be fine; the underlying isabelle latex already includes an appro-
priate path specification for T
E
Xinputs.
If the text contains any references to Isabelle symbols (such as \<forall>)
then isabellesym.sty should be included as well. This package contains a
standard set of L
A
T
E
Xmacro definitions \isasymfoo corresponding to \<foo>,
see [1] for a complete list of predefined Isabelle symbols. Users may invent
further symbols as well, just by providing L
A
T
E
Xmacros in a similar fashion
as in ~~/lib/texinputs/isabellesym.sty of the Isabelle distribution.
For proper setup of DVI and PDF documents (with hyperlinks and book-
marks), we recommend toinclude~~/lib/texinputs/pdfsetup.sty aswell.
As a final step of Isabelle document preparation, isabelle document -c is
run on the resulting copy of the document directory. Thus the actual output
document is built and installed in its proper place. The generated sources
are deleted after successful run of L
A
T
E
Xand friends.
Some care is needed if the document output location is configured differently,
say within a directory whose content is still required afterwards!
3.4 Running L
A
T
E
X within the Isabelle envi-
ronment
The isabelle latex tool provides the basic interface for Isabelle document
preparation. Its usage is:
Usage: isabelle latex [OPTIONS] [FILE]
Options are:
-o FORMAT
specify output format: pdf (default), dvi,
bbl, idx, sty, syms
Run LaTeX (and related tools) on FILE (default root.tex),
producing the specified output format.
Appropriate L
A
T
E
X-related programs are run on the input file, according to
the given output format: latex, pdflatex, dvips, bibtex (for bbl), and
makeindex (for idx). The actual commands are determined from the settings
environment (ISABELLE_PDFLATEX etc.).
CHAPTER 3. PRESENTING THEORIES
26
The sty output format causes the Isabelle style files to be updated from the
distribution. This is useful in special situations where the document sources
are to be processed another time by separate tools.
The syms output is for internal use; it generates lists of symbols that are
available without loading additional L
A
T
E
Xpackages.
Examples
Invoking isabelle latex by hand may be occasionally useful when debug-
ging failed attempts of the automatic document preparation stage of batch-
mode Isabelle. The abortive process leaves the sources at a certain place
within ISABELLE_BROWSER_INFO, see the runtime error message for details.
This enables users to inspect L
A
T
E
Xruns in further detail, e.g. like this:
cd "$(isabelle getenv -b ISABELLE_BROWSER_INFO)/Unsorted/Test/document"
isabelle latex -o pdf
Chapter 4
Isabelle/Scala development
tools
Isabelle/ML and Isabelle/Scala are the two main language environments for
Isabelle tool implementations. There are some basic command-line tools
to work with the underlying Java Virtual Machine, the Scala toplevel and
compiler. Notethat Isabelle/jEdit [3] provides a Scala Console for interactive
experimentation within the running application.
4.1 Java
Runtime
Environment
within
Isabelle
The isabelle java tool is a direct wrapper for the Java Runtime Environ-
ment, within the regular Isabelle settings environment (§1.1). The command
line arguments are that of the underlying Java version. It is run in -server
mode if possible, to improve performance (at the cost of extra startup time).
The java executable is the one within ISABELLE_JDK_HOME, according to the
standard directory layout for official JDK distributions. The class loader
is augmented such that the name space of Isabelle/Pure.jar is available,
which is the main Isabelle/Scala module.
For example, the following command-line invokes the main method of class
isabelle.GUI_Setup, which opens a windows with some diagnostic infor-
mation about the Isabelle environment:
isabelle java isabelle.GUI_Setup
4.2 Scala toplevel
The isabelle scala tool is a direct wrapper for the Scala toplevel; see
also isabelle java above. The command line arguments are that of the
underlying Scala version.
27
Documents you may be interested
Documents you may be interested