1.1 --- a/src/HOL/SPARK/Tools/spark_vcs.ML Thu Dec 10 09:16:44 2020 +0100
1.2 +++ b/src/HOL/SPARK/Tools/spark_vcs.ML Thu Dec 10 14:38:32 2020 +0100
1.3 @@ -32,6 +32,11 @@
1.4 (** theory data **)
1.5
1.6 fun err_unfinished () = error "An unfinished SPARK environment is still open."
1.7 +(*
1.8 + ERROR: Found the end of the theory, but the last SPARK environment is still open.
1.9 + ..is OK, since "spark_end" does NOT work here for some reason.
1.10 +fun err_unfinished () = ()
1.11 +*)
1.12
1.13 val strip_number = apply2 implode o chop_suffix Fdl_Lexer.is_digit o raw_explode;
1.14
2.1 --- a/src/Pure/Isar/proof.ML Thu Dec 10 09:16:44 2020 +0100
2.2 +++ b/src/Pure/Isar/proof.ML Thu Dec 10 14:38:32 2020 +0100
2.3 @@ -395,6 +395,16 @@
2.4 else [];
2.5
2.6 val position_markup = Position.markup (Position.thread_data ()) Markup.position;
2.7 +(*//---------------------------- test code: NO @{print} available ------------------------\\* )
2.8 + val part1 = [Pretty.block
2.9 + [Pretty.mark_str (position_markup, "proof"), Pretty.str (" (" ^ mode_name mode ^ ")")]]
2.10 + val part3 = (if verbose orelse mode = Forward then
2.11 + pretty_sep (pretty_facts ctxt "" (Option.map #1 facts)) (prt_goal (try find_goal state))
2.12 + else if mode = Chain then pretty_facts ctxt "picking" (Option.map #1 facts)
2.13 + else prt_goal (try find_goal state))
2.14 +(*------------------------------ test code: NO @{print} available --------------------------*)
2.15 + val _ = @{print} {a = "pretty_state:", part1 = part1, part3 = part3}
2.16 +( *\\---------------------------- test code: NO @{print} available ------------------------//*)
2.17 in
2.18 [Pretty.block
2.19 [Pretty.mark_str (position_markup, "proof"), Pretty.str (" (" ^ mode_name mode ^ ")")]] @
3.1 --- a/src/Pure/Thy/document_source.ML Thu Dec 10 09:16:44 2020 +0100
3.2 +++ b/src/Pure/Thy/document_source.ML Thu Dec 10 14:38:32 2020 +0100
3.3 @@ -90,6 +90,15 @@
3.4
3.5 val tag_scope =
3.6 Parse.group (fn () => "document tag scope") (Parse.$$$ "(" |-- Parse.!!! (scope --| Parse.$$$ ")"));
3.7 +(*//---------------------------- test code: NO @{print} available ------------------------\\* )
3.8 +fun tag_scope toks =
3.9 + let
3.10 + val xxx =
3.11 + (Parse.group (fn () => "document tag scope")
3.12 + (Parse.$$$ "(" |-- Parse.!!! (scope --| Parse.$$$ ")"))) toks
3.13 + val _ = @{print} {a = "Document_Source.tag_scope", result = xxx}
3.14 + in xxx end;
3.15 +( *\\---------------------------- test code: NO @{print} available ------------------------//*)
3.16
3.17 val tag_name =
3.18 Parse.group (fn () => "document tag name") (Parse.short_ident || Parse.string);
4.1 --- a/src/Tools/isac/BridgeJEdit/Calculation.thy Thu Dec 10 09:16:44 2020 +0100
4.2 +++ b/src/Tools/isac/BridgeJEdit/Calculation.thy Thu Dec 10 14:38:32 2020 +0100
4.3 @@ -151,6 +151,7 @@
4.4 subsubsection \<open>copied from spark_vcs.ML\<close>
4.5 ML \<open>
4.6 \<close> ML \<open>
4.7 +(**)
4.8 fun err_unfinished () = error "An unfinished SPARK environment is still open."
4.9 \<close> ML \<open>
4.10 val strip_number = apply2 implode o chop_suffix Fdl_Lexer.is_digit o raw_explode;
4.11 @@ -694,6 +695,7 @@
4.12 prove_vc\<close>
4.13
4.14 subsection \<open>test runs with Example\<close>
4.15 +subsubsection \<open>with new code\<close>
4.16 text \<open>
4.17 Starting the Calculation for the Example requires session Isac with Isac.Biegelinie etc.
4.18 So, do ~~$ ./zcoding-to-test.sh and use Test_Some.thy to evaluate
4.19 @@ -702,9 +704,18 @@
4.20
4.21 This now gives no error, but also no <Output>. See child of 3ea616c84845.
4.22 \<close>
4.23 -(*required for proof below..*)
4.24 -spark_proof_functions
4.25 - gcd = "gcd :: int \<Rightarrow> int \<Rightarrow> int"
4.26 +
4.27 +subsubsection \<open>with original SPARK code\<close>
4.28 +text \<open>
4.29 + The sequence of code below is copied from SPARK/Examples/Gcd/Greatest_Common_Divisor.thy.
4.30 + But here the code works only partially (see ERROR at end).
4.31 + Thus it is advisable to run tests in Greatest_Common_Divisor.thy.
4.32 +
4.33 + spark_proof_functions is required for proof below..
4.34 +\<close>
4.35 +(*//------------------- outcomment before creating session Isac ----------------------------\\* )
4.36 +(**)
4.37 + spark_proof_functions gcd = "gcd :: int \<Rightarrow> int \<Rightarrow> int"
4.38 (**)
4.39 spark_open \<open>~~/src/HOL/SPARK/Examples/Gcd/greatest_common_divisor/g_c_d\<close>
4.40 (*Output..* )
4.41 @@ -735,6 +746,8 @@
4.42 spark_end
4.43 ( *Bad path binding: "$ISABELLE_HOME/src/HOL/SPARK/Examples/Gcd/greatest_common_divisor/g_c_d.prv"*)
4.44
4.45 +( *\\------------------- outcomment before creating session Isac ----------------------------//*)
4.46 +
4.47
4.48 section \<open>adapt spark_vc to Problem\<close>
4.49
4.50 @@ -788,7 +801,7 @@
4.51 \<close>
4.52
4.53
4.54 -end(*
4.55 +end(* SEE "outcomment before creating session Isac" ABOVE !!! OTHERWISE YOU HAVE..
4.56 ERROR: Found the end of the theory, but the last SPARK environment is still open.
4.57 - ..is OK, since "spark_end" does NOT work here for some reason.
4.58 + ..is acceptable for testing spark_vc .. proof - ...
4.59 *)
5.1 --- a/src/Tools/isac/BridgeJEdit/parseC.sml Thu Dec 10 09:16:44 2020 +0100
5.2 +++ b/src/Tools/isac/BridgeJEdit/parseC.sml Thu Dec 10 14:38:32 2020 +0100
5.3 @@ -33,7 +33,7 @@
5.4 val tokenize: string -> Token.T list
5.5 val string_of_toks: Token.T list -> string
5.6 val parse: (Token.T list -> 'a * Token.T list) -> Token.T list -> 'a * Token.T list
5.7 -(*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\*)
5.8 +(*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
5.9
5.10 (*Model*)
5.11 type model
5.12 @@ -72,7 +72,7 @@
5.13 val parse_form_refs: Fdl_Lexer.T list -> form_refs * Fdl_Lexer.T list;
5.14 val parse_form_model: Fdl_Lexer.T list -> string list * Fdl_Lexer.T list;
5.15 val parse_string : Fdl_Lexer.T list -> string * Fdl_Lexer.T list;
5.16 -(*\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
5.17 +( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
5.18 end
5.19
5.20 (**)