--- a/ProgTutorial/Base.thy Wed May 28 12:41:09 2014 +0100
+++ b/ProgTutorial/Base.thy Tue Jul 08 11:34:10 2014 +0100
@@ -1,10 +1,6 @@
theory Base
imports Main
"~~/src/HOL/Library/LaTeXsugar"
-(*keywords "ML" "setup" "local_setup" :: thy_decl and
- "ML_prf" :: prf_decl and
- "ML_val" :: diag
-*)
begin
notation (latex output)
--- a/ProgTutorial/Essential.thy Wed May 28 12:41:09 2014 +0100
+++ b/ProgTutorial/Essential.thy Tue Jul 08 11:34:10 2014 +0100
@@ -175,12 +175,13 @@
Hint: The third term is already quite big, and the pretty printer
may omit parts of it by default. If you want to see all of it, you
- can use the following ML-function to set the printing depth to a higher
- value:
-
- @{ML [display,gray] "default_print_depth 50"}
+ need to set the printing depth to a higher value by
\end{exercise}
-
+*}
+
+declare [[ML_print_depth = 50]]
+
+text {*
The antiquotation @{text "@{prop \<dots>}"} constructs terms by inserting the
usually invisible @{text "Trueprop"}-coercions whenever necessary.
Consider for example the pairs
--- a/ProgTutorial/First_Steps.thy Wed May 28 12:41:09 2014 +0100
+++ b/ProgTutorial/First_Steps.thy Tue Jul 08 11:34:10 2014 +0100
@@ -1,8 +1,7 @@
theory First_Steps
imports Base
begin
-
-
+
chapter {* First Steps\label{chp:firststeps} *}
text {*
@@ -98,7 +97,7 @@
@{ML_response_fake [display,gray] "writeln \"any string\"" "\"any string\""}
- will print out @{text [quotes] "any string"} inside the response buffer.
+ will print out @{text [quotes] "any string"}.
This function expects a string as argument. If you develop under
PolyML, then there is a convenient, though again ``quick-and-dirty'', method
for converting values into strings, namely the antiquotation
@@ -114,11 +113,12 @@
@{ML_response_fake [display,gray]
"if 0 = 1 then true else (error \"foo\")"
-"Exception- ERROR \"foo\" raised
-At command \"ML\"."}
+"*** foo
+***"}
This function raises the exception @{text ERROR}, which will then
- be displayed by the infrastructure. Note that this exception is meant
+ be displayed by the infrastructure indicating that it is an error by
+ painting the output red. Note that this exception is meant
for ``user-level'' error messages seen by the ``end-user''.
For messages where you want to indicate a genuine program error, then
use the exception @{text Fail}.
@@ -152,7 +152,7 @@
text {*
You can also print out terms together with their typing information.
- For this you need to set the configuration value
+ For this you need to set the configuration value
@{ML_ind show_types in Syntax} to @{ML true}.
*}
@@ -543,7 +543,7 @@
can be implemented more concisely as
*}
-ML %grayML{*fun separate i [] = ([], [])
+ML %grayML{*fun separate _ [] = ([], [])
| separate i (x::xs) =
if i <= x
then separate i xs ||> cons x
@@ -772,15 +772,17 @@
difference between a theory and a context is will be described in Chapter
\ref{chp:advanced}.) A context is for example needed in order to use the
function @{ML print_abbrevs in Proof_Context} that list of all currently
- defined abbreviations.
+ defined abbreviations. For example
@{ML_response_fake [display, gray]
"Proof_Context.print_abbrevs @{context}"
-"Code_Evaluation.valtermify \<equiv> \<lambda>x. (x, \<lambda>u. Code_Evaluation.termify x)
+"\<dots>
INTER \<equiv> INFI
Inter \<equiv> Inf
\<dots>"}
+ The precise output of course depends on the abbreviations that are
+ currently defined; this can change over time.
You can also use antiquotations to refer to proved theorems:
@{text "@{thm \<dots>}"} for a single theorem
@@ -812,14 +814,14 @@
and the second is a proof. For example
*}
-ML %grayML{*val foo_thm = @{lemma "True" and "False \<Longrightarrow> P" by simp_all} *}
+ML %grayML{*val foo_thms = @{lemma "True" and "False \<Longrightarrow> P" by simp_all} *}
text {*
The result can be printed out as follows.
@{ML_response_fake [gray,display]
-"foo_thm |> pretty_thms_no_vars @{context}
- |> pwriteln"
+"foo_thms |> pretty_thms_no_vars @{context}
+ |> pwriteln"
"True, False \<Longrightarrow> P"}
You can also refer to the current simpset via an antiquotation. To illustrate
@@ -915,10 +917,9 @@
setup %gray {* type_pat_setup *}
-text {*
- However, a word of warning is in order: Introducing new antiquotations
- should be done only after careful deliberations. They can make your
- code harder to read, than making it easier.
+text {*
+However, a word of warning is in order: Introducing new antiquotations should be done only after
+careful deliberations. They can potentially make your code harder to read, than making it easier.
\begin{readmore}
The files @{ML_file "Pure/ML/ml_antiquotation.ML"} and @{ML_file "Pure/ML/ml_antiquotations.ML"}
@@ -992,10 +993,10 @@
Notice that we access the integer as an integer and the boolean as
a boolean. If we attempt to access the integer as a boolean, then we get
a runtime error.
-
+
@{ML_response_fake [display, gray]
"project_bool (nth foo_list 0)"
-"*** Exception- Match raised"}
+"*** exception Match raised"}
This runtime error is the reason why ML is still type-sound despite
containing a universal type.
@@ -1216,7 +1217,7 @@
for treating theories and proof contexts more uniformly. This type is defined as follows
*}
-ML_val{*datatype generic =
+ML_val %grayML{*datatype generic =
Theory of theory
| Proof of proof*}
--- a/ProgTutorial/Intro.thy Wed May 28 12:41:09 2014 +0100
+++ b/ProgTutorial/Intro.thy Tue Jul 08 11:34:10 2014 +0100
@@ -4,6 +4,7 @@
chapter {* Introduction *}
+
text {*
\begin{flushright}
{\em
@@ -22,7 +23,9 @@
and implement new ideas. The source code of Isabelle can look intimidating,
but beginners can get by with knowledge of only a handful of concepts,
a small number of functions and a few basic coding conventions.
-
+ There is also a considerable amount of code written in Scala that allows
+ Isabelle interface with the Jedit GUI. Explanation of this part is beyond
+ this tutorial.
The best way to get to know the ML-level of Isabelle is by experimenting
with the many code examples included in the tutorial. The code is as far as
--- a/ProgTutorial/Recipes/TimeLimit.thy Wed May 28 12:41:09 2014 +0100
+++ b/ProgTutorial/Recipes/TimeLimit.thy Tue Jul 08 11:34:10 2014 +0100
@@ -22,7 +22,7 @@
Now the call
- @{ML_response_fake [display,gray] "ackermann (4, 12)" "\<dots>"}
+ @{ML_response_fake_both [display,gray] "ackermann (4, 12)" "\<dots>"}
takes a bit of time before it finishes. To avoid this, the call can be encapsulated
in a time limit of five seconds. For this you have to write
--- a/ProgTutorial/antiquote_setup.ML Wed May 28 12:41:09 2014 +0100
+++ b/ProgTutorial/antiquote_setup.ML Tue Jul 08 11:34:10 2014 +0100
@@ -31,6 +31,9 @@
fun ml_type txt =
implode ["val _ = NONE : (", txt, ") option"];
+fun ml_out txt =
+ implode ["val _ = Pretty.writeln ((Pretty.from_ML (pretty_ml (PolyML.prettyRepresentation ((", txt, "), ML_Options.get_print_depth ()))))) handle _ => writeln \"exception\""]
+
(* eval function *)
fun eval_fn ctxt exp =
ML_Context.eval_source_in (SOME ctxt) ML_Compiler.flags
@@ -82,18 +85,18 @@
(* checks and expression agains a result pattern *)
fun output_response {context = ctxt, ...} (lhs, pat) =
(eval_fn ctxt (ml_pat (lhs, pat));
- (*write_file_ml_blk lhs (Proof_Context.theory_of ctxt);*)
+ eval_fn ctxt (ml_out lhs);
output ctxt ((prefix_lines "" lhs) @ (prefix_lines "> " pat)))
(* checks the expressions, but does not check it against a result pattern *)
fun output_response_fake {context = ctxt, ...} (lhs, pat) =
(eval_fn ctxt (ml_val [] NONE lhs);
- (*write_file_ml_blk lhs (Proof_Context.theory_of ctxt);*)
+ eval_fn ctxt (ml_out lhs);
output ctxt ((split_lines lhs) @ (prefix_lines "> " pat)))
(* checks the expressions, but does not check it against a result pattern *)
fun ouput_response_fake_both {context = ctxt, ...} (lhs, pat) =
- output ctxt ((split_lines lhs) @ (prefix_lines "> " pat))
+ (output ctxt ((split_lines lhs) @ (prefix_lines "> " pat)))
val single_arg = Scan.lift (Args.name)
val two_args = Scan.lift (Args.name -- Args.name)
Binary file progtutorial.pdf has changed