synchronized Session.update;
authorwenzelm
Sat Mar 17 18:18:53 2018 +0100 (14 months ago)
changeset 67893c854e50c2114
parent 67892 25e2b621bdcb
child 67894 fee080c4045f
synchronized Session.update;
src/Pure/Thy/thy_resources.scala
     1.1 --- a/src/Pure/Thy/thy_resources.scala	Sat Mar 17 17:23:35 2018 +0100
     1.2 +++ b/src/Pure/Thy/thy_resources.scala	Sat Mar 17 18:18:53 2018 +0100
     1.3 @@ -204,43 +204,41 @@
     1.4          new Thy_Resources.Theory(node_name, node_header, text, true)
     1.5        }
     1.6  
     1.7 -    val edits =
     1.8 -      state.change_result(st =>
     1.9 -        {
    1.10 -          val st1 = st.insert_required(id, dep_theories)
    1.11 -          val theory_edits =
    1.12 -            for (theory <- loaded_theories)
    1.13 -            yield {
    1.14 -              val node_name = theory.node_name
    1.15 -              val theory1 = theory.required(st1.is_required(node_name))
    1.16 -              val edits = theory1.node_edits(st1.theories.get(node_name))
    1.17 -              (edits, (node_name, theory1))
    1.18 -            }
    1.19 -          (theory_edits.flatMap(_._1), st1.update_theories(theory_edits.map(_._2)))
    1.20 -        })
    1.21 -    session.update(Document.Blobs.empty, edits)
    1.22 +    state.change(st =>
    1.23 +      {
    1.24 +        val st1 = st.insert_required(id, dep_theories)
    1.25 +        val theory_edits =
    1.26 +          for (theory <- loaded_theories)
    1.27 +          yield {
    1.28 +            val node_name = theory.node_name
    1.29 +            val theory1 = theory.required(st1.is_required(node_name))
    1.30 +            val edits = theory1.node_edits(st1.theories.get(node_name))
    1.31 +            (edits, (node_name, theory1))
    1.32 +          }
    1.33 +        session.update(Document.Blobs.empty, theory_edits.flatMap(_._1))
    1.34 +        st1.update_theories(theory_edits.map(_._2))
    1.35 +      })
    1.36  
    1.37      dep_theories
    1.38    }
    1.39  
    1.40    def unload_theories(session: Session, id: UUID, dep_theories: List[Document.Node.Name])
    1.41    {
    1.42 -    val edits =
    1.43 -      state.change_result(st =>
    1.44 -        {
    1.45 -          val st1 = st.remove_required(id, dep_theories)
    1.46 -          val theory_edits =
    1.47 -            for {
    1.48 -              node_name <- dep_theories
    1.49 -              theory <- st1.theories.get(node_name)
    1.50 -            }
    1.51 -            yield {
    1.52 -              val theory1 = theory.required(st1.is_required(node_name))
    1.53 -              val edits = theory1.node_edits(Some(theory))
    1.54 -              (edits, (node_name, theory1))
    1.55 -            }
    1.56 -          (theory_edits.flatMap(_._1), st1.update_theories(theory_edits.map(_._2)))
    1.57 -        })
    1.58 -    session.update(Document.Blobs.empty, edits)
    1.59 +    state.change(st =>
    1.60 +      {
    1.61 +        val st1 = st.remove_required(id, dep_theories)
    1.62 +        val theory_edits =
    1.63 +          for {
    1.64 +            node_name <- dep_theories
    1.65 +            theory <- st1.theories.get(node_name)
    1.66 +          }
    1.67 +          yield {
    1.68 +            val theory1 = theory.required(st1.is_required(node_name))
    1.69 +            val edits = theory1.node_edits(Some(theory))
    1.70 +            (edits, (node_name, theory1))
    1.71 +          }
    1.72 +        session.update(Document.Blobs.empty, theory_edits.flatMap(_._1))
    1.73 +        st1.update_theories(theory_edits.map(_._2))
    1.74 +      })
    1.75    }
    1.76  }