ftuong
/
draft
1
0
Fork 0
Code Issues Pull Requests Releases Wiki Activity

upgrade to Isabelle2019

This commit is contained in:
Burkhart Wolff 2019-07-12 15:15:55 +02:00 committed by Frédéric Tuong
parent b25a89c2f4
commit 051e4e4281
1 changed files with 19 additions and 17 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

36
Example_Markup.thy
View File

@ -60,24 +60,24 @@ fun report [] _ _ = I
ML \<open>
local
val data = \<comment> \<open>Derived from Yakoub's example ;-)\<close>
[ (\<open>Frédéric 1er\<close>, \<open>King of Naples\<close>)
, (\<open>Frédéric II\<close>, \<open>King of Sicily\<close>)
, (\<open>Frédéric III\<close>, \<open>the Handsome\<close>)
, (\<open>Frédéric IV\<close>, \<open>of the Empty Pockets\<close>)
, (\<open>Frédéric V\<close>, \<open>King of Denmark–Norway\<close>)
, (\<open>Frédéric VI\<close>, \<open>the Knight\<close>)
, (\<open>Frédéric VII\<close>, \<open>Count of Toggenburg\<close>)
[ (\<open>Frédéric 1er\<close>, \<open>King of Naples\<close>)
, (\<open>Frédéric II\<close>, \<open>King of Sicily\<close>)
, (\<open>Frédéric III\<close>, \<open>the Handsome\<close>)
, (\<open>Frédéric IV\<close>, \<open>of the Empty Pockets\<close>)
, (\<open>Frédéric V\<close>, \<open>King of Denmark–Norway\<close>)
, (\<open>Frédéric VI\<close>, \<open>the Knight\<close>)
, (\<open>Frédéric VII\<close>, \<open>Count of Toggenburg\<close>)
, (\<open>Frédéric VIII\<close>, \<open>Count of Zollern\<close>)
, (\<open>Frédéric IX\<close>, \<open>the Old\<close>)
, (\<open>Frédéric X\<close>, \<open>the Younger\<close>) ]
, (\<open>Frédéric IX\<close>, \<open>the Old\<close>)
, (\<open>Frédéric X\<close>, \<open>the Younger\<close>) ]
val (tab0, markup) =
fold_map (fn (name, msg) => fn reports =>
let val id = serial ()
val pos = [Input.pos_of name]
in
( (Input.source_content msg, (name, pos, id))
, report pos (markup_tvar NONE pos) (Input.source_content name, id) reports)
( (fst(Input.source_content msg), (name, pos, id))
, report pos (markup_tvar NONE pos) (fst(Input.source_content name), id) reports)
end)
data
[]
@ -93,19 +93,21 @@ val _ =
fold (fn input =>
let
val pos1' = Input.pos_of input
fun ctnt name0 = fst(Input.source_content name0)
val pos1 = [pos1']
val msg1 = Input.source_content input
val msg1 = fst(Input.source_content input)
val msg2 = "No persons were found to have such nickname"
in
case Symtab.lookup tab (Input.source_content input) of
NONE => tap (fn _ => Output.information ("No persons were found to have such nickname" ^ Position.here_list pos1))
case Symtab.lookup tab (fst(Input.source_content input)) of
NONE => tap (fn _ => Output.information (msg2 ^ Position.here_list pos1))
(cons ((pos1', Markup.bad ()), ""))
| SOME (name0, pos0, id) => report pos1 (markup_tvar (SOME (Input.source_content name0)) pos0) (msg1, id)
| SOME (name0, pos0, id) => report pos1 (markup_tvar (SOME (ctnt name0)) pos0) (msg1, id)
end)
[ \<open>the Knight\<close> \<comment> \<open>Example of a correct retrieval (CTRL + Hovering shows what we are expecting)\<close>
[ \<open>the Knight\<close> \<comment> \<open>Example of a correct retrieval (CTRL + Hovering shows what we are expecting)\<close>
, \<open>the Handsome\<close> \<comment> \<open>Example of a correct retrieval (CTRL + Hovering shows what we are expecting)\<close>
, \<open>the Spy\<close> \<comment> \<open>Example of a failure to retrieve the person in \<^ML>\<open>tab\<close>\<close> ]
[]
|> Position.reports_text
\<close>
end
end