forked from Isabelle_DOF/Isabelle_DOF
Working on
- the Toplevel sync problem for LaTeX output - attribute computation - various syntax issues - examples.
This commit is contained in:
parent
aeb235447c
commit
6277f44e75
122
Isa_DOF.thy
122
Isa_DOF.thy
|
|
@ -607,79 +607,12 @@ end (* struct *)
|
|||
text{* fghfgh *}
|
||||
|
||||
text*[sdf] {* f @{thm refl}*}
|
||||
ML{* AnnoTextelemParser.SPY2;
|
||||
(* conclusion: Input.source_explode converts " f @{thm refl}"
|
||||
into:
|
||||
[(" ", {offset=14, id=-2769}), ("f", {offset=15, id=-2769}), (" ", {offset=16, id=-2769}),
|
||||
("@", {offset=17, id=-2769}), ("{", {offset=18, id=-2769}), ("t", {offset=19, id=-2769}),
|
||||
("h", {offset=20, id=-2769}), ("m", {offset=21, id=-2769}), (" ", {offset=22, id=-2769}),
|
||||
("r", {offset=23, id=-2769}), ("e", {offset=24, id=-2769}), ("f", {offset=25, id=-2769}),
|
||||
("l", {offset=26, id=-2769}), ("}", {offset=27, id=-2769})]
|
||||
*)*}
|
||||
|
||||
text*[sdfg] {* fg @{thm refl}*}
|
||||
ML{* AnnoTextelemParser.SPY3; *}
|
||||
|
||||
ML{*
|
||||
(* text is :
|
||||
|
||||
val _ =
|
||||
Outer_Syntax.command ("text", @{here}) "formal comment (primary style)"
|
||||
(Parse.opt_target -- Parse.document_source >> Thy_Output.document_command {markdown = true});
|
||||
|
||||
*)
|
||||
(* registrierung *)
|
||||
Outer_Syntax.command : Outer_Syntax.command_keyword -> string
|
||||
-> (Toplevel.transition -> Toplevel.transition) parser -> unit;
|
||||
|
||||
(* Isar Toplevel Steuerung *)
|
||||
Toplevel.keep : (Toplevel.state -> unit) -> Toplevel.transition -> Toplevel.transition;
|
||||
(* val keep' = add_trans o Keep;
|
||||
fun keep f = add_trans (Keep (fn _ => f));
|
||||
*)
|
||||
|
||||
Toplevel.present_local_theory : (xstring * Position.T) option -> (Toplevel.state -> unit) ->
|
||||
Toplevel.transition -> Toplevel.transition;
|
||||
(* fun present_local_theory target = present_transaction (fn int =>
|
||||
(fn Theory (gthy, _) =>
|
||||
let val (finish, lthy) = Named_Target.switch target gthy;
|
||||
in Theory (finish lthy, SOME lthy) end
|
||||
| _ => raise UNDEF));
|
||||
|
||||
fun present_transaction f g = add_trans (Transaction (f, g));
|
||||
fun transaction f = present_transaction f (K ());
|
||||
*)
|
||||
|
||||
Toplevel.theory : (theory -> theory) -> Toplevel.transition -> Toplevel.transition;
|
||||
(* fun theory' f = transaction (fn int =>
|
||||
(fn Theory (Context.Theory thy, _) =>
|
||||
let val thy' = thy
|
||||
|> Sign.new_group
|
||||
|> f int
|
||||
|> Sign.reset_group;
|
||||
in Theory (Context.Theory thy', NONE) end
|
||||
| _ => raise UNDEF));
|
||||
|
||||
fun theory f = theory' (K f); *)
|
||||
|
||||
Thy_Output.document_command : {markdown: bool} -> (xstring * Position.T) option * Input.source ->
|
||||
Toplevel.transition -> Toplevel.transition;
|
||||
(* fun document_command markdown (loc, txt) =
|
||||
Toplevel.keep (fn state =>
|
||||
(case loc of
|
||||
NONE => ignore (output_text state markdown txt)
|
||||
| SOME (_, pos) =>
|
||||
error ("Illegal target specification -- not a theory context" ^ Position.here pos))) o
|
||||
Toplevel.present_local_theory loc (fn state => ignore (output_text state markdown txt));
|
||||
|
||||
*)
|
||||
|
||||
Thy_Output.output_text : Toplevel.state -> {markdown: bool} -> Input.source -> string ;
|
||||
(* this is where antiquotation expansion happens : uses eval_antiquote *)
|
||||
|
||||
|
||||
*}
|
||||
|
||||
ML{* AnnoTextelemParser.SPY3;
|
||||
(* produces: ref "fg \\isa{<markup>\\ {\\isacharequal}\\ <markup>}": string ref *)
|
||||
(* This proves that Thy_Output.output_text(Toplevel.theory_toplevel thy) markdown toks actually
|
||||
PRODUCES strings in which the antiquotations were expanded. *)
|
||||
*}
|
||||
(* <<< experiments *)
|
||||
|
||||
section{* Syntax for Ontological Antiquotations (the '' View'' Part II) *}
|
||||
|
|
@ -792,24 +725,42 @@ fun calculate_attr_access ctxt proj_term term =
|
|||
val Const(@{const_name "HOL.eq"},_) $ lhs $ _ = HOLogic.dest_Trueprop (Thm.concl_of thm)
|
||||
in lhs end
|
||||
|
||||
fun calculate_attr_access_check ctxt proj_str str = (* template *)
|
||||
let val term = Bound 0
|
||||
in (ML_Syntax.atomic o ML_Syntax.print_term) term
|
||||
end
|
||||
fun calculate_attr_access_check ctxt attr oid = (* template *)
|
||||
case DOF_core.get_value_local oid ctxt of
|
||||
SOME term => let val SOME{cid,...} = DOF_core.get_object_local oid ctxt
|
||||
val (pr_name,_,ty) = case DOF_core.get_attribute_long_name_local cid attr ctxt of
|
||||
SOME f => f
|
||||
| NONE => error ("attribute undefined for ref"^ oid)
|
||||
val proj_term = Const(pr_name,ty) (* pr_name should be long_name *)
|
||||
val term = calculate_attr_access ctxt proj_term term
|
||||
in (ML_Syntax.atomic o ML_Syntax.print_term) term end
|
||||
| NONE => error "identifier not a docitem reference"
|
||||
|
||||
*}
|
||||
|
||||
ML{*
|
||||
ML_Syntax.atomic o ML_Syntax.print_term;
|
||||
Args.term --| (Scan.lift @{keyword "in"}) -- Args.term;
|
||||
fn (ctxt,toks) =>
|
||||
(Scan.lift Args.name --| (Scan.lift @{keyword "in"}) -- Args.term >>
|
||||
(fn(attr_term, class_term) => (ML_Syntax.atomic o ML_Syntax.print_term) class_term)) (ctxt, toks);
|
||||
Scan.lift Args.name --| (Scan.lift @{keyword "in"}) -- Scan.lift Args.name;
|
||||
(fn (ctxt,toks) =>
|
||||
(Scan.lift Args.name --| (Scan.lift @{keyword "in"}) -- Scan.lift Args.name >>
|
||||
(fn(attr, oid) => (calculate_attr_access_check (Context.the_proof ctxt) attr oid) )) (ctxt, toks))
|
||||
: string context_parser
|
||||
|
||||
*}
|
||||
ML{*
|
||||
val _ = Theory.setup
|
||||
( ML_Antiquotation.inline @{binding doc_class_attr} (Args.term >> (ML_Syntax.atomic o ML_Syntax.print_term)))
|
||||
|
||||
(ML_Antiquotation.inline @{binding doc_class_attr}
|
||||
(fn (ctxt,toks) =>
|
||||
(Scan.lift Args.name --|
|
||||
(Scan.lift @{keyword "in"}) --
|
||||
Scan.lift Args.name
|
||||
>>
|
||||
(fn(attr : string, oid : string) =>
|
||||
(calculate_attr_access_check (Context.the_proof ctxt) attr oid) )
|
||||
: string context_parser
|
||||
)
|
||||
(ctxt, toks))
|
||||
)
|
||||
*}
|
||||
|
||||
|
||||
|
|
@ -906,10 +857,12 @@ end (* struct *)
|
|||
|
||||
*}
|
||||
|
||||
text*[xxxy] {* dd @{docitem_ref \<open>sdfg\<close>} @{thm refl}}*}
|
||||
text*[xxxy] {* dd @{docitem_ref \<open>sdfg\<close>} @{thm refl}*}
|
||||
|
||||
ML{* AnnoTextelemParser.SPY3; *}
|
||||
|
||||
|
||||
text{* dd @{docitem_ref \<open>sdfg\<close>} @{thm refl} *}
|
||||
|
||||
section{* Library of Standard Text Ontology *}
|
||||
|
||||
datatype placement = pl_h | pl_t | pl_b | pl_ht | pl_hb
|
||||
|
|
@ -933,7 +886,6 @@ doc_class side_by_side_figure = figure +
|
|||
|
||||
(* dito the future monitor: table - block *)
|
||||
|
||||
ML{* open Mixfix;*}
|
||||
section{* Testing and Validation *}
|
||||
|
||||
|
||||
|
|
|
|||
|
|
@ -364,6 +364,17 @@ ML\<open>val X = @{here};\<close>
|
|||
|
||||
*}
|
||||
|
||||
subsection {*Input streams. *}
|
||||
ML{*
|
||||
Input.source_explode : Input.source -> Symbol_Pos.T list;
|
||||
(* conclusion: Input.source_explode converts " f @{thm refl}"
|
||||
into:
|
||||
[(" ", {offset=14, id=-2769}), ("f", {offset=15, id=-2769}), (" ", {offset=16, id=-2769}),
|
||||
("@", {offset=17, id=-2769}), ("{", {offset=18, id=-2769}), ("t", {offset=19, id=-2769}),
|
||||
("h", {offset=20, id=-2769}), ("m", {offset=21, id=-2769}), (" ", {offset=22, id=-2769}),
|
||||
("r", {offset=23, id=-2769}), ("e", {offset=24, id=-2769}), ("f", {offset=25, id=-2769}),
|
||||
("l", {offset=26, id=-2769}), ("}", {offset=27, id=-2769})]
|
||||
*)*}
|
||||
|
||||
subsection {*Scanning and combinator parsing. *}
|
||||
ML\<open>
|
||||
|
|
@ -400,14 +411,17 @@ Parse.nat: int parser;
|
|||
Parse.int: int parser;
|
||||
Parse.enum_positions: string -> 'a parser -> ('a list * Position.T list) parser;
|
||||
Parse.enum: string -> 'a parser -> 'a list parser;
|
||||
Parse.input: 'a parser -> Input.source parser;
|
||||
|
||||
Parse.enum;
|
||||
Parse.!!!;
|
||||
Parse.enum : string -> 'a parser -> 'a list parser;
|
||||
Parse.!!! : (T list -> 'a) -> T list -> 'a;
|
||||
Parse.position: 'a parser -> ('a * Position.T) parser;
|
||||
|
||||
(* Examples *)
|
||||
Parse.position Args.cartouche_input;
|
||||
\<close>
|
||||
|
||||
text{* Parsing combinators for elementary Isabelle Lexems*}
|
||||
ML{*
|
||||
Syntax.parse_sort;
|
||||
Syntax.parse_typ;
|
||||
|
|
@ -456,27 +470,36 @@ fn name => (Thy_Output.antiquotation name (Scan.lift (Parse.position Args.cartou
|
|||
\<close>
|
||||
|
||||
subsection\<open> Markup \<close>
|
||||
text{* Markup Operations, and reporting. Diag in Isa_DOF Foundations Paper. *}
|
||||
text{* Markup Operations, and reporting. Diag in Isa_DOF Foundations Paper.
|
||||
Markup operation send via side-effect annotations to the GUI (precisely:
|
||||
to the PIDE Framework) that were used for hyperlinking applicating to binding
|
||||
occurrences, info for hovering, ... *}
|
||||
ML{*
|
||||
(* Markup.enclose; *)
|
||||
|
||||
(* Position.report is also a type consisting of a pair of a position and markup. *)
|
||||
(* It would solve all my problems if I find a way to infer the defining Position.report
|
||||
from a type definition occurence ... *)
|
||||
|
||||
Position.report;
|
||||
Position.reports; (* ? ? ? I think this is the magic thing that sends reports to the GUI. *)
|
||||
|
||||
Markup.properties;
|
||||
Properties.get;
|
||||
Position.report: Position.T -> Markup.T -> unit;
|
||||
Position.reports: Position.report list -> unit;
|
||||
(* ? ? ? I think this is the magic thing that sends reports to the GUI. *)
|
||||
Markup.entity : string -> string -> Markup.T;
|
||||
Markup.properties : Properties.T -> Markup.T -> Markup.T ;
|
||||
Properties.get : Properties.T -> string -> string option;
|
||||
Markup.enclose : Markup.T -> string -> string;
|
||||
|
||||
|
||||
fun theory_markup def name id pos =
|
||||
(* example for setting a link, the def flag controls if it is a defining or a binding
|
||||
occurence of an item *)
|
||||
fun theory_markup (def:bool) (name:string) (id:serial) (pos:Position.T) =
|
||||
if id = 0 then Markup.empty
|
||||
else
|
||||
Markup.properties (Position.entity_properties_of def id pos)
|
||||
(Markup.entity Markup.theoryN name);
|
||||
Markup.theoryN;
|
||||
Markup.theoryN : string;
|
||||
|
||||
serial(); (* A global, lock-guarded seriel counter used to produce unique identifiers,
|
||||
be it on the level of thy-internal states or as reference in markup in
|
||||
PIDE *)
|
||||
|
||||
(* From Theory:
|
||||
fun check ctxt (name, pos) =
|
||||
|
|
@ -510,9 +533,7 @@ fun get_markup thy =
|
|||
|
||||
|
||||
*)
|
||||
serial(); (* A global, lock-guarded seriel counter used to produce unique identifiers,
|
||||
be it on the level of thy-internal states or as reference in markup in
|
||||
PIDE *)
|
||||
|
||||
(*
|
||||
fun theory_markup def thy_name id pos =
|
||||
if id = 0 then Markup.empty
|
||||
|
|
@ -553,8 +574,6 @@ fun check ctxt (name, pos) =
|
|||
|
||||
|
||||
*)
|
||||
Markup.properties; (* read : add Properties.T items into Markup.T *)
|
||||
Markup.entity;
|
||||
|
||||
*}
|
||||
|
||||
|
|
@ -663,7 +682,6 @@ fun control_antiquotation name s1 s2 =
|
|||
|
||||
Output.output;
|
||||
|
||||
Proof_Context.read_const;
|
||||
Syntax.read_input ;
|
||||
Input.source_content;
|
||||
|
||||
|
|
@ -738,13 +756,23 @@ fun output_text state {markdown} source =
|
|||
*}
|
||||
|
||||
|
||||
ML{* Outer_Syntax.print_commands @{theory};
|
||||
ML{*
|
||||
Outer_Syntax.print_commands @{theory};
|
||||
|
||||
Outer_Syntax.command : Outer_Syntax.command_keyword -> string ->
|
||||
(Toplevel.transition -> Toplevel.transition) parser -> unit;
|
||||
(* creates an implicit thy_setup with an entry for a call-back function, which happens
|
||||
to be a parser that must have as side-effect a Toplevel-transition-transition. *)
|
||||
|
||||
to be a parser that must have as side-effect a Toplevel-transition-transition.
|
||||
Registers "Toplevel.transition -> Toplevel.transition" parsers to the Isar interpreter.
|
||||
*)
|
||||
|
||||
(*Example: text is :
|
||||
|
||||
val _ =
|
||||
Outer_Syntax.command ("text", @{here}) "formal comment (primary style)"
|
||||
(Parse.opt_target -- Parse.document_source >> Thy_Output.document_command {markdown = true});
|
||||
*)
|
||||
|
||||
(* not exported: Thy_Output.output_token; Ich glaub, da passierts ... *)
|
||||
Thy_Output.present_thy;
|
||||
*}
|
||||
|
|
@ -798,6 +826,8 @@ fun document_antiq check_file ctxt (name, pos) =
|
|||
ML{* Type_Infer_Context.infer_types *}
|
||||
ML{* Type_Infer_Context.prepare_positions *}
|
||||
|
||||
|
||||
|
||||
section {*Transaction Management in the Isar-Engine : The Toplevel *}
|
||||
|
||||
ML{*
|
||||
|
|
@ -827,8 +857,108 @@ Toplevel.present_local_theory:
|
|||
Toplevel.present_local_theory loc (fn state => ignore (output_text state markdown txt)); *)
|
||||
Thy_Output.document_command : {markdown: bool} -> (xstring * Position.T) option * Input.source ->
|
||||
Toplevel.transition -> Toplevel.transition;
|
||||
|
||||
(* Isar Toplevel Steuerung *)
|
||||
Toplevel.keep : (Toplevel.state -> unit) -> Toplevel.transition -> Toplevel.transition;
|
||||
(* val keep' = add_trans o Keep;
|
||||
fun keep f = add_trans (Keep (fn _ => f));
|
||||
*)
|
||||
|
||||
Toplevel.present_local_theory : (xstring * Position.T) option -> (Toplevel.state -> unit) ->
|
||||
Toplevel.transition -> Toplevel.transition;
|
||||
(* fun present_local_theory target = present_transaction (fn int =>
|
||||
(fn Theory (gthy, _) =>
|
||||
let val (finish, lthy) = Named_Target.switch target gthy;
|
||||
in Theory (finish lthy, SOME lthy) end
|
||||
| _ => raise UNDEF));
|
||||
|
||||
fun present_transaction f g = add_trans (Transaction (f, g));
|
||||
fun transaction f = present_transaction f (K ());
|
||||
*)
|
||||
|
||||
Toplevel.theory : (theory -> theory) -> Toplevel.transition -> Toplevel.transition;
|
||||
(* fun theory' f = transaction (fn int =>
|
||||
(fn Theory (Context.Theory thy, _) =>
|
||||
let val thy' = thy
|
||||
|> Sign.new_group
|
||||
|> f int
|
||||
|> Sign.reset_group;
|
||||
in Theory (Context.Theory thy', NONE) end
|
||||
| _ => raise UNDEF));
|
||||
|
||||
fun theory f = theory' (K f); *)
|
||||
|
||||
Thy_Output.document_command : {markdown: bool} -> (xstring * Position.T) option * Input.source ->
|
||||
Toplevel.transition -> Toplevel.transition;
|
||||
(* fun document_command markdown (loc, txt) =
|
||||
Toplevel.keep (fn state =>
|
||||
(case loc of
|
||||
NONE => ignore (output_text state markdown txt)
|
||||
| SOME (_, pos) =>
|
||||
error ("Illegal target specification -- not a theory context" ^ Position.here pos))) o
|
||||
Toplevel.present_local_theory loc (fn state => ignore (output_text state markdown txt));
|
||||
|
||||
*)
|
||||
|
||||
Thy_Output.output_text : Toplevel.state -> {markdown: bool} -> Input.source -> string ;
|
||||
(* this is where antiquotation expansion happens : uses eval_antiquote *)
|
||||
|
||||
|
||||
*}
|
||||
|
||||
|
||||
ML{*
|
||||
|
||||
|
||||
(* Isar Toplevel Steuerung *)
|
||||
Toplevel.keep : (Toplevel.state -> unit) -> Toplevel.transition -> Toplevel.transition;
|
||||
(* val keep' = add_trans o Keep;
|
||||
fun keep f = add_trans (Keep (fn _ => f));
|
||||
*)
|
||||
|
||||
Toplevel.present_local_theory : (xstring * Position.T) option -> (Toplevel.state -> unit) ->
|
||||
Toplevel.transition -> Toplevel.transition;
|
||||
(* fun present_local_theory target = present_transaction (fn int =>
|
||||
(fn Theory (gthy, _) =>
|
||||
let val (finish, lthy) = Named_Target.switch target gthy;
|
||||
in Theory (finish lthy, SOME lthy) end
|
||||
| _ => raise UNDEF));
|
||||
|
||||
fun present_transaction f g = add_trans (Transaction (f, g));
|
||||
fun transaction f = present_transaction f (K ());
|
||||
*)
|
||||
|
||||
Toplevel.theory : (theory -> theory) -> Toplevel.transition -> Toplevel.transition;
|
||||
(* fun theory' f = transaction (fn int =>
|
||||
(fn Theory (Context.Theory thy, _) =>
|
||||
let val thy' = thy
|
||||
|> Sign.new_group
|
||||
|> f int
|
||||
|> Sign.reset_group;
|
||||
in Theory (Context.Theory thy', NONE) end
|
||||
| _ => raise UNDEF));
|
||||
|
||||
fun theory f = theory' (K f); *)
|
||||
|
||||
Thy_Output.document_command : {markdown: bool} -> (xstring * Position.T) option * Input.source ->
|
||||
Toplevel.transition -> Toplevel.transition;
|
||||
(* fun document_command markdown (loc, txt) =
|
||||
Toplevel.keep (fn state =>
|
||||
(case loc of
|
||||
NONE => ignore (output_text state markdown txt)
|
||||
| SOME (_, pos) =>
|
||||
error ("Illegal target specification -- not a theory context" ^ Position.here pos))) o
|
||||
Toplevel.present_local_theory loc (fn state => ignore (output_text state markdown txt));
|
||||
|
||||
*)
|
||||
|
||||
Thy_Output.output_text : Toplevel.state -> {markdown: bool} -> Input.source -> string ;
|
||||
(* this is where antiquotation expansion happens : uses eval_antiquote *)
|
||||
|
||||
|
||||
*}
|
||||
|
||||
|
||||
subsection\<open> Configuration flags of fixed type in the Isar-engine. \<close>
|
||||
|
||||
ML{*
|
||||
|
|
|
|||
|
|
@ -87,10 +87,10 @@ text*[q1::Task, level="oneStar", mark="1::int", type="formal"]
|
|||
subsubsection*[exo3 :: Exercise, Exercise.content="[q1::Task,q2::Task]"]\<open>Exercise 3\<close>
|
||||
|
||||
text*[q2::Task, level="threeStars", mark="3::int", type="formal"]
|
||||
{*
|
||||
Prove that @{term "n*(n+5) + 2*(n+3) "} is always the product of two numbers
|
||||
with a difference of 5.
|
||||
*}
|
||||
|
||||
{* Prove that @{term "n*(n+5) + 2*(n+3) "} is always the product of two numbers
|
||||
with a difference of 5.
|
||||
*}
|
||||
(* this does not work on the level of the LaTeX output for known restrictions of the Toplevel. *)
|
||||
close_monitor*[exam::MathExam]
|
||||
|
||||
end
|
||||
|
|
|
|||
Loading…
Reference in New Issue